Formalizing Flajolet and Sedgewick’s Analytic Combinatorics in Lean 4, one chapter at a time, is a slow campaign. Chapter VII — applications of singularity analysis — runs into two counting results about trees.

The first is Cayley’s formula. A rooted labelled tree on $n$ vertices is a tree on the vertex set $\{1,\dots,n\}$ with one vertex marked as the root. There are exactly $n^{\,n-1}$ of them.

The second counts ternary trees: a ternary tree is either empty, or a root carrying three ordered ternary subtrees (left, middle, right). Counting by the number $n$ of internal nodes, the answer is the Fuss–Catalan number

Neither number is in doubt. The problem is how they entered the formalization: both were written down by fiat, as closed forms. The code literally defined cayleyRootedTree n := n^(n-1) and ternaryTreeCount n := C(3n,n)/(2n+1). So the statement “$n^{\,n-1}$ counts the trees” was never derived from an actual combinatorial object — it was installed as a definition. An audit pass caught it: the asymptotic analysis built on top is real, but it is the asymptotics of a closed-form sequence, not of a proven tree count. The job was to turn “this counts the trees” into a theorem — to build the genuine combinatorial object and prove its cardinality equals the closed form.

Two hard roads

The textbook proofs of these two facts are both heavy going.

Cayley’s formula is usually proved with the Prüfer sequence: a bijection between labelled trees on $n$ vertices and sequences in $\{1,\dots,n\}^{n-2}$, so the number of trees equals the number of sequences, $n^{n-2}$ (times $n$ for the choice of root). The bijection is easy to describe; the pain in a formal proof is showing the two maps are mutually inverse — repeatedly “remove the smallest leaf, record its neighbour,” then prove decoding exactly reconstructs the encoding. That invariant is notoriously fiddly.

The ternary count is worse. The classical route is a Rothe–Hagen / Raney convolution identity. We hoped to reuse the Gosper-summation trick that Mathlib already uses for the Catalan numbers — but it doesn’t transfer. We checked: in the cubic case the summand is simply not Gosper-summable. The quadratic (Catalan) case is, which is why Mathlib has that one; the cubic case is not, so that road never existed. Both results are “submit a new library to Mathlib” in size.

We were about to start grinding. Then the problem turned.

The same key

The formalization of the same book had, back in Chapter I, already proved one thing: Lagrange inversion for formal power series.

Lagrange inversion reads coefficients off a functional equation. If a power series $T$ with $T(0)=0$ satisfies

for some series $\varphi$ with $\varphi(0)\neq 0$, then for every $n\ge 1$ its $n$-th coefficient has a clean closed form,

The right-hand side no longer mentions $T$: if you can extract a coefficient of a power of $\varphi$, you can read off the coefficient of $T$.

And both tree counts are, at heart, Lagrange-inversion problems — because the recursive structure of a tree is a functional equation. Write the counting series for each family. For labelled rooted trees we use the exponential generating function (EGF), the natural bookkeeping for labelled objects,

for ternary trees we use the ordinary generating function (OGF),

Now translate the recursive definition of each family into an equation on its series. A rooted labelled tree is a root together with a set of rooted labelled subtrees; under the EGF dictionary the “set of” construction becomes $\exp$, and the root contributes one factor of $z$. A ternary tree is either empty (the constant $1$) or a root with three ordered ternary subtrees, which under the OGF becomes a cube. So the two series satisfy

Both are of the form to feed into the one key.

Rooted trees. Take $\varphi=\exp$, so $T=z\,e^{T}=z\,\varphi(T)$. Lagrange inversion gives

Since $[z^n]T = t_n/n!$, multiplying by $n!$ gives $t_n = n^{\,n-1}$ — Cayley.

Ternary trees. The constant term is in the way, so shift: let $T=B-1$. Then $T = z\,B^3 = z\,(1+T)^3$, i.e. $T=z\,\varphi(T)$ with $\varphi(w)=(1+w)^3$. For $n\ge 1$,

A one-line binomial rearrangement turns $\tfrac1n\binom{3n}{n-1}$ into $\tfrac{1}{2n+1}\binom{3n}{n}$ — the Fuss–Catalan number.

One key, two locks. No Prüfer, no Rothe–Hagen. The two “submit a library” roads were both dissolved by a single tool that Chapter I had already put on the shelf. In Lean this is exactly what the closing theorems say: a genuine recursive object (RootedLTree — a root plus a partition of the remaining labels into children, recursively trees; and the inductive ternary tree) is built, its cardinality is computed through the functional equation and Lagrange inversion, and that cardinality is proved equal to the banked closed form. Both proofs go through with the cleanest possible logical footprint.

Coincidence is the shadow of preparedness

This looks like luck — Chapter I just happened to have the right tool. It is not luck.

When Chapter I proved Lagrange inversion, it was “merely” a topic in Chapter I. One could have proved only the special case needed at the time and moved on. Instead it was proved in full generality — the theorem for an arbitrary $\varphi$, together with the uniqueness of the series solving $T=z\varphi(T)$. So when Chapter VII hit a wall, the tool was already on the shelf — our own shelf.

Thorough preparation pays off in a way that is often non-local: the foundation you pour at point A holds up a wall at an unrelated point B. Mathematics is connected; the more completely you prove one thing, the more “coincidentally” it serves you later. What looks like a coincidence is the shadow cast by sufficiency — you do the preparation properly, and only then does luck have somewhere to land.

There is a second half, about knowing. A tool on the shelf is no use if you don’t reach for it; you have to know what you already own. Remembering “Chapter I has Lagrange inversion” was possible only because the earlier chapters had been read through first, leaving a map of the toolkit in mind. Half of capability is the tools; the other half is knowing where they are and how far their light reaches. Stock the library, then learn it by heart — and coincidences will start happening to you more and more often.

Dans les champs de l’observation, le hasard ne favorise que les esprits préparés.

In the fields of observation, chance favors only the prepared mind. — Louis Pasteur, 1854