Machine-Checked Arithmetic Bit Complexity of the Kannan-Bachem Smith Normal Form in Lean 4
Junye Ji
cs.LO
Jul 24, 2026 · v2
cs.DS cs.SC
TL;DR
Formalizes the Kannan-Bachem Smith normal form algorithm in Lean 4 over Mathlib, proving its correctness, termination, and polynomial arithmetic bit-complexity bounds.
Abstract
We formalize in Lean 4 the Kannan-Bachem Smith normal form algorithm for nonsingular square integer matrices. The program returns $S,U,U^{-1},V,V^{-1}$ and proves $UAV=S$, $U^{-1}SV^{-1}=A$, four inverse identities, the Smith divisibility conditions, and equality of $S$ with a canonical reference matrix. Stabilization terminates because each recursive pass strictly decreases the binary size of the active pivot; the outer algorithm recurses on the lower-right block. The computation also emits a flat trace of designated sign-magnitude arithmetic leaves. Branch conditions, quotients, Bezout data, and matrix entries are taken from the recorded primitive runs. Composite phases form their traces by concatenating the charge lists returned by the executed children. Verified self-delimiting codecs define the input and output sizes. Coefficient and work recurrences, closed by a kernel-checked polynomial-envelope calculus, give fixed polynomial bounds for both trace cost and the encoded length of the five output matrices. The theorem concerns these arithmetic primitives; structural operations and compiled Lean runtime are outside the model.
Problem
Computing the Smith normal form of an integer matrix risks intermediate coefficient blow-up. Kannan and Bachem gave a polynomial-time algorithm, but no machine-checked proof of its correctness and bit complexity existed.
Approach
The algorithm for nonsingular square integer matrices is implemented in Lean 4 over Mathlib. It returns S, U, U^{-1}, V and V^{-1}, together with proofs of the transformation and inverse identities, the Smith divisibility conditions, and equality of S with a canonical reference matrix. Termination of the stabilization step uses strict decrease of Nat.size of the pivot, while the outer recursion decreases the matrix dimension. Executions emit traces of sign-magnitude arithmetic primitives; verified prefix-free codecs define input and output sizes, and a kernel-checked polynomial-envelope calculus closes the cost recurrences.
Results
The development proves fixed polynomial bounds on both the arithmetic trace cost and the encoded output length, in terms of the encoded input length. The resulting envelope degrees are coarse: 2,150,687 for cost and 98,990 for output size. Structural operations and compiled Lean runtime are outside the cost model.
