Walks that Forget the Cycles: A Machine-Checked Bijection between Tree-Like Walks and Godsil's Path Tree in Lean 4 (Part III)

Part III of the godsil-gutman-lean series. A machine-checked, sorry-free proof in Lean 4 / Mathlib of the combinatorial half of Godsil's moment theorem: the tree-like closed walks of a finite graph G at a vertex v are in length-preserving bijection with the closed walks at the root of Godsil's path tree T(G,v), via the down-projection π. The tree-like walk count is thus a sum of adjacency-matrix powers of the path trees, and (each path tree being a forest) its matching polynomial is the characteristic polynomial of its adjacency matrix. The spectral half completing p_k = Σ θ_i^k is mapped, not built. All cited theorems depend only on propext, Classical.choice and Quot.sound. Formalized with AI assistance (Claude, Anthropic); the mathematics and all claims are the author's responsibility. English and Spanish editions; source and figures at github.com/karlesmarin/godsil-gutman-lean.