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

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ₖ = Σ θᵢᵏ 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.