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_k = tr(Bk), where A is the adjacency matrix, B the Hashimoto non-backtracking operator, and p_k 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_k; 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.