What a Determinant's Derivative Knows: Jacobi's Formula and Newton's Identity for Matrix Traces in Lean 4

A machine-checked formalization, in Lean 4 / Mathlib, of Jacobi's formula (det M)′ = tr(adj M·M′) for a matrix of polynomials, and of Newton's identity for matrix traces — the logarithmic derivative of the reversed characteristic polynomial collects the trace power sums, (charpolyRev M)′ = −charpolyRev M·∑k tr(Mk+1)Xk. The engine is a resolvent series (I−XM)−1 = ∑k MkXk over formal power series. As an application these compose with the author's earlier formalization of Bass's determinant formula (doi:10.5281/zenodo.20573120) to read the Ihara non-backtracking counts Nk = tr(Bk) off the adjacency spectrum, and to prove combinatorially that tr(Bk) counts closed non-backtracking walks. All headline results are sorry-free (axioms: propext, Classical.choice, Quot.sound). It formalizes classical mathematics and claims no new theorem; the novelty is the formalization — Jacobi's algebraic formula and the matrix-trace Newton identity, for which a search of Mathlib, the Isabelle/HOL Archive of Formal Proofs, Coq/Rocq, HOL Light and Mizar found no prior machine-checked proof. Honest boundary: tr(Bk) counts rooted closed walks, not geodesic classes, and the prime-geodesic Euler product is mapped, not built. English and Spanish editions are included.