HEXAGONbeta

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

A mix of human-written and AI-generated textHuman understanding: some partsmath.CO — Combinatoricscs.LO — Logic in Computer Science

Contributed by Peter W. Murphy, MD ↗

Version 1 / Oct 27, 2026 / CC BY 4.0

Abstract

For a tree TT with Laplacian L(T)L(T), Brualdi and Goldwasser (1984) introduced the Laplacian ratio π(T)=per⁡L(T)/∏vdeg⁡v\pi(T)=\operatorname{per} L(T)/\prod_v\deg v and asked which tree on nn vertices maximizes it. We answer the question for every nn. For every n≥4n\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≥492n\ge 492 the centre carries only arms, almost all with five cherries, and the exceptional arms are fixed by 6(n−1) mod 116(n-1)\bmod 11 through an explicit rule; for 4≤n≤4914\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, 64621ρn≤max⁡∣T∣=nπ(T)≤2ρn−1\tfrac{64}{621}\rho^{n}\le\max_{|T|=n}\pi(T)\le 2\rho^{n-1} with ρ=(621/64)1/11\rho=(621/64)^{1/11}, and prove the sharp inequality behind it: every pendant subtree bb has matching weight at most ρ∣b∣\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).

Provenance statement

Text declaration: a mix of human-written and AI-generated. Human-understanding declaration: some parts of this contribution, but not all, have been checked and understood by a human. Additional provenance: the formalization, the certificate generators and much of the exploration and drafting were developed with extensive assistance from Claude (Anthropic), working under the author's direction; the author takes responsibility for the content. The full argument is formalized in Lean 4 with Mathlib and checked by the Lean kernel, depending only on Lean's three standard axioms (propext, Classical.choice, Quot.sound), with no sorry, no native_decide and no added axioms; the main statement was also accepted by a second, independent kernel. The author has checked the formal statement and definitions; independent human refereeing of the full argument is pending. Source, certificates and build: https://github.com/DrMurphyIsIn/brualdi-goldwasser (release v1.4.4, commit 93d140e), doi:10.5281/zenodo.22983412.

Tools used

Anthropic
Claude

References

  1. T. Bousch, La condition de Walters , Ann.\ Sci.\ Éc.\ Norm.\ Supér.\ (4) 34 (2001), 287--311. doi:10.1016/S0012-9593(00)01062-4 (https://doi.org/10.1016/S0012-9593(00)01062-4).DOI
  2. R. A. Brualdi and J. L. Goldwasser, Permanent of the Laplacian matrix of trees and bipartite graphs , Discrete Math.\ 48 (1984), 1--21. doi:10.1016/0012-365X(84)90127-4 (https://doi.org/10.1016/0012-365X(84)90127-4).DOI
  3. P. Csikvári, On a poset of trees , Combinatorica 30 (2010), 125--137. doi:10.1007/s00493-010-2516-0 (https://doi.org/10.1007/s00493-010-2516-0).DOI
  4. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language , in: Automated Deduction -- CADE 28, Lecture Notes in Comput.\ Sci.\ 12699 , Springer, 2021, 625--635.
  5. X. Geng, X. Hu and S. Li, Further results on permanental bounds for the Laplacian matrix of trees , Linear Multilinear Algebra 58 (2010), 571--587. doi:10.1080/03081080902765583 (https://doi.org/10.1080/03081080902765583).DOI
  6. O. J. Heilmann and E. H. Lieb, Theory of monomer-dimer systems , Comm.\ Math.\ Phys.\ 25 (1972), 190--232. doi:10.1007/BF01877590 (https://doi.org/10.1007/BF01877590).DOI
  7. O. Jenkinson, Ergodic optimization in dynamical systems , Ergodic Theory Dynam.\ Systems 39 (2019), 2593--2618. doi:10.1017/etds.2017.142 (https://doi.org/10.1017/etds.2017.142).DOI
  8. Lean FRO, Comparator : checking a Lean proof against a separately written statement, https://github.com/leanprover/comparator (version v4.32.0 ).link
  9. The mathlib Community, The Lean mathematical library , in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, 367--381. doi:10.1145/3372885.3373824 (https://doi.org/10.1145/3372885.3373824).DOI
  10. R. Merris, Laplacian matrices of graphs: a survey , Linear Algebra Appl.\ 197--198 (1994), 143--176. doi:10.1016/0024-3795(94)90486-3 (https://doi.org/10.1016/0024-3795(94)90486-3).DOI
Show all 18 referencesShow fewer references
  1. R. Merris, K. R. Rebman and W. Watkins, Permanental polynomials of graphs , Linear Algebra Appl.\ 38 (1981), 273--288. doi:10.1016/0024-3795(81)90026-4 (https://doi.org/10.1016/0024-3795(81)90026-4).DOI
  2. M. Mézard and A. Montanari, Information, Physics, and Computation , Oxford Graduate Texts, Oxford University Press, 2009.
  3. C. Bailey, nanoda_lib : a type checker for the Lean 4 kernel language, https://github.com/ammkrn/nanoda_lib.link
  4. P. Pant, Counterexamples to a conjecture on Laplacian ratios of trees , arXiv:2605.14176 (2026).arXiv
  5. L. G. Valiant, The complexity of computing the permanent , Theoret.\ Comput.\ Sci.\ 8 (1979), 189--201. doi:10.1016/0304-3975(79)90044-6 (https://doi.org/10.1016/0304-3975(79)90044-6).DOI
  6. S. Wagner and I. Gutman, Maxima and minima of the Hosoya index and the Merrifield--Simmons index: a survey of results and techniques , Acta Appl.\ Math.\ 112 (2010), 323--346. doi:10.1007/s10440-010-9575-5 (https://doi.org/10.1007/s10440-010-9575-5).DOI
  7. T. Wu, X. Dong and H.-J. Lai, Two problems on Laplacian ratios of trees , Discrete Appl.\ Math.\ 372 (2025), 224--236. doi:10.1016/j.dam.2025.04.047 (https://doi.org/10.1016/j.dam.2025.04.047).DOI
  8. T. Wu, X. Dong, H.-J. Lai and X. Zeng, Solution to an open problem on Laplacian ratio , Front.\ Math.\ 21 (2026), no. 4, 815--837. doi:10.1007/s11464-024-0191-5 (https://doi.org/10.1007/s11464-024-0191-5); arXiv:2402.15669 (2024).arXivDOI

Version history

  1. v1Submitted by Peter W. Murphy, MDInitial depositCurrentOct 26, 2026