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

v2 (correction): Fixed an imprecise claim in the introduction. The matching polynomial is not the characteristic polynomial of the graph's adjacency matrix unless the graph is a forest — the earlier wording (“of no matrix” / “no symmetric matrix”) was false, since every monic polynomial is the char. poly. of its companion matrix and, being real-rooted, of a diagonal (symmetric) matrix. The Lean formalization and theorem are unchanged. Thanks to Scott Hotton for the correction. 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_k(G) = Σ_i θ_i^k = treeLikeWalkCount(G,k) (matchingPowerSum_eq_treeLikeWalkCount). 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_identity into reversed matching polynomials; both the walk-count and the root-power-sum generating functions are forced to the same reflected derivative reflect_n(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.