Peter W. Murphy, MD

math.CO — Combinatorics

The maximum Laplacian ratio of a tree: a complete answer to a question of Brualdi and Goldwasser, kernel-checked in Lean

Contributed by Peter W. Murphy, MD

For a tree $T$ with Laplacian $L(T)$, Brualdi and Goldwasser (1984) introduced the Laplacian ratio $\pi(T)=\operatorname{per} L(T)/\prod_v\deg v$ and asked which tree on $n$ vertices maximizes it. We answer the question for every $n$. For every $n\ge 4$ the maximum is attained by a spider of cherry arms: a centre carrying pendant paths of length two (cherries) and arms, an arm being a vertex that carries cherries. For $n\ge 492$ the centre carries only arms, almost all with five cherries, and the exceptional arms are fixed by $6(n-1)\bmod 11$ through an explicit rule; for $4\le n\le 491$ the maximizer is given by an explicit table. Along the way we determine the exact exponential growth rate of the maximum, $\tfrac{64}{621}\rho^{n}\le\max_{|T|=n}\pi(T)\le 2\rho^{n-1}$ with $\rho=(621/64)^{1/11}$, and prove the sharp inequality behind it: every pendant subtree $b$ has matching weight at most $\rho^{|b|}$, with equality exactly for the five-cherry arm. The whole argument is formalized in Lean 4 with Mathlib and checked by the Lean kernel, depending only on Lean's three standard axioms. Large parts of it are certificates: exact data produced by untrusted generators and checked by the kernel. We explain the mathematics, show where each piece lives in the formal development and why it is organized that way, and discuss what the answer and the method suggest. Code, certificates and the Lean formalization: https://github.com/DrMurphyIsIn/brualdi-goldwasser (release v1.4.4; Zenodo doi:10.5281/zenodo.22983412).