Unfolding a Graph into a Tree: A Machine-Checked Proof of the Heilmann-Lieb Theorem in Lean 4 (Part II)

A machine-checked formalization, in Lean 4 / Mathlib, of the Heilmann-Lieb theorem: the matching polynomial mu_G of every finite graph is real-rooted, and for maximum degree Delta >= 2 all its roots lie in the Ramanujan band [-2 sqrt(Delta-1), 2 sqrt(Delta-1)]. The proof follows Godsil's path tree: unfold G into the tree T(G,u) of its paths (where the matching polynomial equals a characteristic polynomial) and transport back along the divisibility mu_G | mu_{T(G,u)}; the root bound is proved from scratch by a weighted Gershgorin / Collatz-Wielandt argument reduced to two facts about distances in a tree. All headline theorems are sorry-free (axioms: propext, Classical.choice, Quot.sound). It formalizes classical mathematics and claims no new theorem; the novelty is the formalization, supported by a search of the Lean/Mathlib, Isabelle/AFP and Coq/mathcomp ecosystems. Lean sources: github.com/karlesmarin/godsil-gutman-lean. English and Spanish editions are included, with the full Lean 4 sources.