When Walks Become a Spectrum: A Machine-Checked Proof of Godsil's Moment Theorem in Lean 4

Part IV of the godsil-gutman-lean series. A machine-checked, sorry-free proof in Lean 4 / Mathlib of Godsil's moment theorem: for a finite graph, the power sums of the roots of the matching polynomial equal the number of closed tree-like walks, pₖ (G) = Σᵢ θᵢᵏ = treeLikeWalkCount (G, k) (matchingPowerSumₑqₜreeLikeWalkCount). Part III built the combinatorial half and mapped the spectral half; this paper builds it and closes the theorem. Each path tree's root–root resolvent is folded through Part II's godsilᵢdentity into reversed matching polynomials; both the walk-count and the root-power-sum generating functions are forced to the same reflected derivative reflectₙ (X·μ'), and a unit is cancelled. The completion needs no univariate Newton recursion — a geometric-series / reversed-product cancellation replaces it. Along the way it contributes general, Mathlib-absent lemmas (a principal-minor determinant collapse for an arbitrary finite index, a reflection-of-a-sum identity, the reverse of a split product). With the Bass companion, both sides of the finite matching/Ihara trace formula now stand sorry-free in one library. The headline depends only on the three standard axioms (propext, Classical. choice, Quot. sound). Includes English and Spanish manuscripts and the LaTeX sources. The formalization and manuscript were developed with AI assistance (Claude, Anthropic) ; the author set the research targets, judged the mathematics, and is responsible for all claims.