In 1984 Brualdi and Goldwasser asked which tree on n vertices maximizes π(T) = per L(T) / ∏ deg(v). This project answers the question for every n, with a proof checked by the Lean kernel.
The certificates behind the proof were produced with Telperion. See it at work in the Telperion Registry Explorer, which puts this theorem first.
A cherry is a pendant path of length two. An arm Aj is a vertex, hanging from a centre, that carries j cherries. A spider of cherry arms is a centre whose branches are all leaves, cherries or arms.
The weight of a pendant subtree is a matching sum, and the five-cherry arm A5 (11 vertices) has weight exactly 621/64. We prove that every pendant subtree b has weight at most ρ|b| with ρ = (621/64)1/11 ≈ 1.22948, and that A5 is the only one attaining it. So the maximum grows exactly like ρn:
(64/621) ρn ≤ max|T|=n π(T) ≤ 2 ρn−1
A maximizer uses as many five-cherry arms as the arithmetic of n allows. The residue n−1 mod 11 is absorbed by a few A4 (9 vertices) or A6 (13 vertices), and which of those wins is a delicate second-order competition, which is why the thresholds 722 and 2319 appear.
Why five, rather than four or six? Give every matched edge an extra weight λ: as λ grows, the best arm climbs 3, 4, 5, 6, … and runs off to infinity at 1 + √5, where the golden ratio appears. Brualdi and Goldwasser's λ = 1 sits on the five-cherry rung. See Why five: the ladder. Along the whole ladder, for every λ > 0, the best block is now known to set the growth rate of πλ: a computer-assisted result (interval arithmetic) up to 1 + √5, extended past it by a short hand argument described on that tab. That cherry regime, λ ≥ 1 + √5, is now also kernel-checked in Lean (formalization/cherry): the ceiling with equality only for the cherry, a strict upper bound for every tree, the lower bound, and the growth rate √(1 + λ/2). For every λ > 0 Lean also checks the one-block formula, that the best branch sets the growth rate, and the witness framework. Below 1 + √5 it now proves the result itself (the inequality, its equality clause and its consequences) on all of 0 < λ < 1 + √5, with no external input: two piecewise-linear witnesses, one on (0, 3/20] and one on [3/20, 1 + √5), whose scalar conditions are all proved in Lean, as exact-rational interval checks over proved monotone enclosures and Bernstein polynomials of degree at most 6.
The maximum divided by ρn−1, for 4 ≤ n ≤ 1200. It stays between the proven bounds, and oscillates with period 11 once the arms settle.
1984: the question. Brualdi and Goldwasser studied the permanent of the Laplacian of trees and bipartite graphs. Over trees on n vertices, the permanent itself is smallest for the star and largest for the path, which mostly rewards having many vertices of degree two. Dividing by the product of the degrees removes that effect, and they introduced the ratio π(T) for that purpose. They proved π(T) ≥ 2, with equality exactly for the star, and posed extremal problems for the ratio, among them the maximum over all trees on n vertices.
2024–2025: the minimum side, and a conjecture. Wu, Dong, Lai and Zeng determined the minimum over trees of diameter at least k (2024), and Wu, Dong and Lai the minimum over trees with a given bipartition (2025). For the maximum, Wu, Dong and Lai conjectured explicit subdivided stars. For odd n: a centre carrying only cherries, with π = 2(3/2)(n−3)/2. For even n: explicit variants in the classes n ≡ 0 and 2 mod 4. Cherries are the best small building block, and for small n the conjecture is right.
2026: counterexamples. P. Pant refuted the conjecture with caterpillars T(a1,…,am): a path whose i-th vertex carries ai cherries. His three families T(3,t,3), T(t,t,t,t) and T(t,t,t+1,t) beat the conjecture from n = 23, 36 and 38, one in each residue class, and he noticed that at n = 21 the tree T(3,3,3) ties the conjectured value. He concluded that the maximum remains open.
How the pieces fit. With the complete answer, the earlier work lines up exactly:
| n | Wu–Dong–Lai conjecture | Pant | the true maximizer |
|---|---|---|---|
| ≤ 22 | correct value | agrees | |
| 21 | C10 (maximal) | T(3,3,3) = C3A32 (maximal) | exactly these two tie |
| 23 | first failure | T(3,4,3) = C4A32 | Pant's tree is the maximizer |
| 24–34 even | correct value | agrees | |
| 36 | first failure (n ≡ 0 mod 4) | T(4,4,4,4) beats it | C4A43 |
| 38 | first failure (n ≡ 2 mod 4) | T(4,4,5,4) beats it | C5A43 |
| ≥ 492 | arms of 4, 5, 6 cherries by the rule |
A caterpillar with three hubs is a spider seen from its middle hub, which is why Pant's T(3,4,3) can be optimal. With four or more hubs it is never a spider, so by the reduction theorem it is never optimal. Wu, Dong and Lai were right that cherries are the basic unit. Pant was right that grouping cherries on several hubs beats a single hub of cherries. The eventual answer is one hub carrying arms, each a second-level hub with exactly five cherries.
Sources: Brualdi & Goldwasser, Discrete Math. 48 (1984); Wu, Dong, Lai & Zeng, Front. Math. 21 (2026) 815–837, arXiv:2402.15669; Wu, Dong & Lai, Discrete Appl. Math. 372 (2025) 224–236; P. Pant, arXiv:2605.14176. The comparisons in the table are computed exactly from the Lean table of maximizers.
Build a tree and watch the three ideas at the heart of the proof work on it. Click a vertex to select it, then add children, remove it, or make it the root. Everything here is computed exactly, in rational arithmetic, in your browser.
A spider is fixed by how many cherries sit at the centre and how many arms of each size it has. Its ratio has a closed form, F = (3/2)c + Σj ∏ αj · (1 + (c/3 + Σ bj)/D), so you can explore the whole family by hand. Change the counts, or scramble a spider and let the balance lemma repair it: whenever the centre has at least three children, moving one cherry from an arm to an arm at least two smaller strictly increases F.
F relative to the optimum for this n, after each move. Balance moves only ever go up.
Why five cherries, and not four or six? Put the problem in a family. Give every matched edge an extra weight λ > 0, so that πλ(T) = ΣM λ|M| ∏uv∈M 1/(deg u deg v). Brualdi and Goldwasser's ratio is λ = 1. For each λ, ask which building block (a leaf, a cherry, or an arm Aj carrying j cherries) gives the most weight per vertex.
Weight per vertex of each block, relative to the cherry: (log T(Aj))/(2j+1) − ½ log((2+λ)/2), for j = 1, …, 12. Above zero the arm beats a plain cherry. The highlighted curve is the best of these blocks at the chosen λ.
A long arm is j cherries plus one hub vertex. The hub is worth adding only if what it buys beats what that same vertex would earn inside a cherry. As j grows the hub multiplies the weight by H(λ) = 2(1+λ)/(2+λ), and a cherry earns ζ(λ) = √((2+λ)/2) per vertex. So long arms win exactly when H > ζ. Squaring and clearing denominators, the balance point is
8(1+λ)2 = (2+λ)3 ⇔ (x−2)(x2−6x+4) = 0 with x = 2+λ, so λ = 0 or λ = 1 ± √5.
At the top of the ladder, λ = 1 + √5, the hub factor and the cherry rate coincide, and both equal the golden ratio φ = (1+√5)/2. The other root, λ = 0, is the bottom of the ladder. There, to first order in λ, the matching sum only sees single edges, and the problem becomes maximizing the Randić index Σuv 1/(deg u deg v), whose maximum over large trees, (15n−1)/56, is attained by spiders of three-cherry arms A3 when n ≡ 1 (mod 7): the bottom rung of the ladder. So one cubic governs the whole ladder, with the Randić index at one end and the golden ratio at the other.
The hub factor H(λ) against the cherry rate ζ(λ). They cross once for λ > 0, at 1 + √5, at height φ.
The ladder says which block is best. A second question is whether that block also sets the growth rate of πλ: whether no pendant subtree of any shape beats the best block per vertex. At λ = 1 that is the sharp ceiling of the Lean proof. It is now proved for every λ > 0, with no gaps: by computer-assisted interval arithmetic (mpmath interval arithmetic, independently re-implemented in Arb) up to 1 + √5, and by a short hand argument from there on. On the whole range the maximal growth rate of πλ is the best-atom rate f*(λ), so the ladder picture above, which arm is best, is the whole story for the growth rate. The proof runs in six regimes:
Real.exp_bound'. This earlier route proves the inequality
only; the equality clause is now proved on the whole range, see the note below.For 0 < λ < 1 + √5 this result is computer-assisted (interval arithmetic). Lean checks the witness framework of this proof for every λ > 0, and now proves the ceiling, its equality clause (equality exactly at the best arms) and its consequences on all of 0 < λ < 1 + √5 with no external input (part_B_full_eq), by a shorter route than the regimes above: two piecewise-linear witnesses, on (0, 3/20] and on [3/20, 1 + √5), whose scalar conditions are all proved in Lean, as exact-rational interval checks over proved monotone enclosures and Bernstein polynomials of degree at most 6. The earlier Lean proofs of the window [3.22, 1 + √5) by hand and of [2, 3.22) by box checks remain in the project. For λ ≥ 1 + √5 it is a hand proof (calculus at 1 + √5 with the golden-ratio identities, then a monotonicity argument), and it is also kernel-checked in Lean (formalization/cherry), by a different route at the anchor. At λ = 1 exactly it is also the sharp ceiling of the Lean proof. For every λ > 0 Lean also checks the one-block formula: with ρ(λ) the supremum of Tb1/|b| over all branches, the maximum lies between Tb⌊(n−1)/|b|⌋ and (1+λ)ρn−1, and its n-th root tends to ρ. Below 1 + √5 the one-block formula alone does not determine ρ(λ); its value there, ef*(λ), comes from the Lean proof of the ceiling on 0 < λ < 1 + √5. It
is about the growth rate only: it says nothing about the shape of the maximizers for λ ≠ 1. As
λ → 0 the rate is governed to first order by the Randić limit above, which is why the bottom
regime is anchored at A3.
What is proved and what is not. The ladder (which block is best among leaves, cherries and arms) and the balance cubic are elementary and proved. At λ = 1, no pendant subtree of any shape beats A5; that is the sharp ceiling in the Lean proof. For every λ > 0 the same ceiling holds: for 0 < λ < 1 + √5 by the computer-assisted (interval arithmetic) arguments above, and in Lean on all of that range (with its equality clause, by two piecewise-linear witnesses), and for λ ≥ 1 + √5 by a hand proof (calculus at the anchor 1 + √5, then a monotonicity argument) that is also kernel-checked in Lean. That the maximizers for other λ are spiders of the best arm is supported by exact computation and is being prepared for publication; treat it as a conjecture for now.
Past the top of the ladder the cherry is the best block, and the claim is that no pendant subtree of any shape beats it per vertex: every planted branch b has Tb(λ) ≤ (1 + λ/2)|b|/2, with equality only for the cherry. Here Tb is the weight of the branch, computed by the cavity recursion: a leaf has T = 1 and message y = 1; a vertex with children c has d = #children + 1, R = Σ yc, Tb = ∏ Tc · (d + λR)/d and yb = 1/(d + λR). The plots below compute it in your browser.
Per-vertex rate of the arms Aj (j cherries on a hub, 2j+1 vertices), fj = log T(Aj)/(2j+1) with T(Aj) = cj(1 + tj/(j+1)), c = 1 + λ/2, t = λ/(2+λ), minus the cherry's rate ½ log(1 + λ/2), for j = 1, …, 12. Every arm is below zero from 1 + √5 on: the cherry is the unique best block.
For each branch, (1/|b|) log(Tb(λ)/(1 + λ/2)|b|/2), which is (1/|b|) log(Tb(λ)/(2+λ)|b|/2) + ½ log 2: the normalized ratio Tb/(2+λ)|b|/2, per vertex and shifted so that the ceiling is the zero line. Every curve is nonincreasing on [2, ∞), and the cherry's is flat at zero. Below 1 + √5 a branch can still sit above zero (A5 does at λ = 2); from the anchor on, none can.
The anchor at λ = 1 + √5, where the ceiling reads Tb ≤ φ|b|, is proved by one-variable calculus using the golden identities 1 + λ/2 = φ2 and 1 + λ = φ3. The extension to every larger λ is the monotonicity drawn above. For λ ≥ 1 + √5 the ceiling, its equality case, the bounds on Mn(λ) below and the growth rate are also kernel-checked in Lean (formalization/cherry); the Lean proof of the anchor takes a different route.
Let Mn(λ) be the largest πλ over trees on n vertices. In the cherry regime the ceiling gives (1 + λ/2)⌊(n−1)/2⌋ ≤ Mn(λ) < (1 + λ)(1 + λ/2)(n−1)/2 for every n ≥ 1, and the upper bound is strict: no tree reaches it. The lower bound comes from a center carrying ⌊(n−1)/2⌋ cherries (and one leaf when n is even). Here Mn is computed exactly as stated, by running the cavity recursion on every tree with n ≤ 12 vertices (987 trees, listed when the page is built); for larger n only the bounds are drawn.
Logarithmic scale, divided by (1+λ/2)(n−1)/2 so that the upper bound is the horizontal line at 1 + λ. The maximum stays strictly below it.
n-th roots: the bounds, and Mn1/n for n ≤ 12, squeeze toward √(1 + λ/2) (dashed), so lim Mn1/n = √(1 + λ/2).
For every λ > 0 the growth rate of Mn(λ) is set by single blocks. Let ρ(λ) be the supremum of Tb1/|b| over all finite planted branches b, the leaf included. Then for every branch b and every n ≥ 1
Tb⌊(n−1)/|b|⌋ ≤ Mn(λ) ≤ (1+λ) ρ(λ)n−1,
ρ(λ) ≤ 1 + λ, lim Mn1/n = ρ(λ).
The lower bound is the tree drawn below: a center carrying k = ⌊(n−1)/|b|⌋ copies of b and the remaining n−1−k|b| vertices as leaves. Pick a branch and an activity.
Per-vertex rate of the branch divided by ρ(λ). A branch touches the line at 1 exactly where it is a best block; the cherry does so for every λ ≥ 1 + √5.
What is checked where. The one-block formula above (the definition of ρ as a supremum, the two bounds, ρ ≤ 1 + λ and the limit) is kernel-checked in Lean for every λ > 0 (formalization/cherry), and so is ρ(λ) = √(1 + λ/2) for λ ≥ 1 + √5. Below 1 + √5, that ρ(λ) = ef*(λ), the best rate among the leaf, the cherry and the arms, is proved in Lean on all of 0 < λ < 1 + √5, with no external input. The curve ρ drawn here uses that value, computed over the cherry and the arms Aj with j ≤ 400 (near 1 + √5 the best arm grows without bound, so the curve is a close lower approximation there). At λ = 1 the arm A5 attains ρ(1) = (621/64)1/11.
For large n almost every arm is A5, and the leftover n−1 mod 11 is absorbed in one of two ways: s arms A6 (13 vertices each) or 11−s arms A4 (9 vertices each), where s = 6(n−1) mod 11. Fours send bigger messages to the centre; sixes waste less weight. Which wins depends on n, and in two classes the answer flips late: at n = 722 and at n = 2319. Pick a class and slide n; the sign is decided in exact arithmetic.
The curve is 106 × (Ffours/Fsixes − 1): above zero the fours win. In the proof, these two late crossings are the only competitions that need Bernstein-basis certificates; the other 221 comparisons are one-sided for every n ≥ 492.
The maximizer for every n: the table (4 ≤ n ≤ 491) is read directly from the
Lean source BGSpiderTableData.lean; beyond it, the rule. Notation: Cc is
c cherries at the centre, Ajm is m arms with j cherries,
L a leaf.
| n | maximizer | centre degree | π / ρn−1 | source |
|---|
At n = 21 two different trees tie: the listed C3A32 and C10. The maximizer is otherwise unique up to isomorphism in every size checked (by exact computation for n ≤ 491 and an exact certificate for n ≥ 2320), but uniqueness is not part of the Lean theorem.
The proof has three layers: a sharp inequality that fixes the growth rate, a reduction showing every maximizer is a spider, and an exact optimization over spiders. Each is split by size.
For a tree, per L(T) = ΣM ∏v unmatched deg v over matchings M, so π(T) = ΣM ∏uv∈M 1/(deg u deg v). A pendant subtree b with root degree d has weight Tb = ∏ Tc (d+R)/d and message yb = 1/(d+R), where R = Σ yc over the children.
Tb ≤ ρ|b| for every pendant subtree, with equality only at A5. Proof: log Tb − |b| log ρ is a sum of per-vertex terms, and an explicit subaction (a potential on vertex states) makes every per-vertex inequality hold, so the sum telescopes. The only tight constraints are the three vertex types of A5, consistent because 27 · 23 = 621.
Lean: R3Cert.BGSCL.bg_sharp, R3Cert.Step3.bg_max_growth
Root at a vertex of maximum degree k. A non-atom child must cost more than it can gain.
A spider's value has a closed form. An exact balance identity shows arm sizes in a maximizer differ
by at most one. For n ≤ 491 the kernel sweeps every balanced configuration (89 chunk files). For
n ≥ 492 exchange arguments confine the maximizer to arms of 4, 5, 6 cherries, and 223 polynomial
certificates (checked by ring and norm_num) pick out the rule.
Read the paper (PDF) for the full argument.
The Lean kernel is the only trusted component. Every certificate was produced by an untrusted generator and is checked by the kernel; a wrong certificate is a failed build.
git clone https://github.com/DrMurphyIsIn/brualdi-goldwasser cd brualdi-goldwasser/formalization lake exe cache get ./build.sh # about 1-2 hours; 96 GB of RAM recommended lake env lean AxiomGuard.lean # every headline theorem: [propext, Classical.choice, Quot.sound] cd .. certificates/verify.sh # regenerate every certificate family, byte-for-byte certificates/verify.sh --full # also the independent certified all-tree search, n <= 491
theorem R3Cert.BGMaximizerAll.bg_maximizer_all_perm (n : Nat) (h4 : 4 <= n)
(t : UTree) (ht : usize t = n) :
(lapl (aGraph (realize (dtRealize t)))).permanent
/ (prod v, (aGraph (realize (dtRealize t))).degree v)
<= (lapl (aGraph (realize (dtRealize (bgMax n))))).permanent
/ (prod v, (aGraph (realize (dtRealize (bgMax n)))).degree v)
Here lapl G has deg on the diagonal and −1 on edges, and
permanent is Mathlib's. What a reviewer should check is that these definitions mean what
they say; the kernel checks the rest.
Table rows and the per-n spider sweep, n ≤ 491.
Envelope tables, tangents and spider bounds, 7 ≤ n ≤ 149.
Credited rate cells and root knapsacks, 150 ≤ n ≤ 491.
The 223 polynomial certificates, n ≥ 492.
Each family has a generator, a frozen Telperion record with hashes, and a driver that regenerates it from scratch and compares it with the frozen copy and with the Lean files. The Telperion Registry Explorer shows the registry these families were developed in, with the Brualdi-Goldwasser campaign in front.
part_B_full): two piecewise-linear
witnesses, on (0, 3/20] and on [3/20, 1 + √5), are witnesses and some arm attains f*, and every scalar
condition is proved in Lean (exact-rational interval checks over proved monotone enclosures, and Bernstein
polynomials of degree at most 6). The equality clause is proved as well (part_B_full_eq,
part_B_equality): equality holds exactly at the best arms. The earlier window results, by hand on [3.22, 1 + √5)
and by 45 exact-rational box checks on [2, 3.22), remain in the project. That project was audited by independent
AI-run audits and replayed by Comparator with nanoda (for the witness framework, (a)–(c) only, the window
statements and part (B) on 0 < λ < 1 + √5; run locally, not sandboxed). The Lean theorem about the maximizer itself is λ = 1 only.