Random Signs into Matchings: A Godsil-Gutman Identity, Formalized in Lean 4 (Part I)

A machine-checked formalization, in Lean 4 / Mathlib, of the Godsil–Gutman identity: the average characteristic polynomial of a uniformly random ±1 signing of a graph is its matching polynomial. The development also contributes the matching polynomial and its deletion recurrence, the ℤ/2 sign-averaging engine, and the Bilu–Linial 2-lift spectral decomposition. The headline theorems are sorry-free (axioms: propext, Classical.choice, Quot.sound). Heilmann–Lieb real-rootedness and interlacing families are mapped, not formalized — a path-tree route is proposed. The paper is included in English and Spanish editions, with figures and exact numerical cross-checks. Lean sources: github.com/karlesmarin/godsil-gutman-lean.