Computing the Smith normal form of nonsingular square integer matrices suffers from intermediate coefficient growth. Verifying both correctness and the polynomial arithmetic bit complexity of such algorithms in a proof assistant is challenging.

The Kannan-Bachem Smith normal form algorithm is implemented in Lean 4 over Mathlib, returning S, U, U^{-1}, V, V^{-1} with proofs of transformation and inverse identities, the Smith divisibility predicate, and equality with a canonical reference matrix. Termination is established via well-founded recursion on the binary size (Nat.size) of the active pivot plus structural recursion on dimension. Executions emit a flat trace of sign-magnitude arithmetic primitives with exact costs, and a polynomial-envelope calculus closes coefficient and work recurrences to yield fixed polynomial bounds. Verified prefix-free codecs define input and output sizes.

The formalization proves correctness of the five-matrix certificate and yields kernel-checked polynomial bounds, with degree 2,150,687 for arithmetic cost and 98,990 for output encoding length. Termination uses exactly two descents, and the polynomial-envelope degree ledger is computed explicitly through all algorithm stages.