The Walks That Remember the Cycles: a machine-checked sharp gap law between the matching polynomial and the non-backtracking spectrum in Lean 4 (Part VI)

A machine-checked, sorry-free proof, in Lean 4 over Mathlib, of the sharp trace-formula gap law for a finite simple graph of girth g: for every 1 ≤ k ≤ g+1, tr (Ak) − pₖ = tr (Bk), where A is the adjacency matrix, B the Hashimoto non-backtracking operator, and pₖ the power sums of the roots of the matching polynomial. Below the girth both sides vanish; at k ∈ g, g+1 both count the rooted traversals of the k-cycles, 2k·cₖ; and the window is sharp — the law fails at k = g+2 on every graph tested, including all 12064 connected cyclic graphs on 4 to 8 vertices. The contribution is the formalization: to the best of the author's knowledge the first machine-checked bridge between the matching polynomial and the non-backtracking spectrum in any proof assistant. The headline theorem depends only on the three standard axioms (propext, Classical. choice, Quot. sound). This is Part VI of the godsil-gutman-lean series. A companion applied paper applies the law, as a certified census of short cycles, to the LDPC codes of the IEEE 802. 11n (WiFi) standard. Formalized with AI assistance (Claude, Anthropic) ; the mathematics and all claims are the author's responsibility.