This repository is the Lean 4 artifact for arXiv:2607.22524. It verifies that one value-producing Kannan--Bachem reduction returns a canonical Smith matrix, four explicit transformation matrices, an execution-derived arithmetic trace, and fixed-polynomial bounds for the trace cost and encoded output length.
The input is a square integer matrix
A : Matrix (Fin n) (Fin n) Int with A.det ≠ 0. Rectangular and singular
matrices, general Euclidean-domain APIs, applications, external generators,
and pre-v0.2 compatibility layers are outside the maintained surface. The
complete boundary is recorded in SCOPE.md.
import NormalForms
#check NormalForms.Research.KannanBachem.VerifiedSmithPolynomialBitCostResult
#check NormalForms.Research.KannanBachem.verifiedSmithPolynomialBitCostverifiedSmithPolynomialBitCost packages the computed
S, U, U⁻¹, V, V⁻¹, the forward and reverse equations, all four inverse
identities, the Smith predicate, equality with the canonical reference, the
exact trace cost, and the two polynomial bounds.
The theorem charges the sign-magnitude addition, multiplication, division, and bounded-XGCD leaves recorded by the executed reduction. It does not claim bounds for structural traversal, allocation, serialization, Lean compilation, native runtime, memory use, or wall-clock time.
The repository pins Lean and mathlib. The complete verification command is:
scripts/verify.shIt builds the artifact, checks the endpoint test and public import closure, audits the ten published roots for unregistered axioms, validates the recorded source identity, and runs the three deterministic Kannan--Bachem cases.
The same command is the container entry point:
docker build --no-cache -f artifact/Dockerfile -t lean-normal-forms:0.2.0-dev .
docker run --rm lean-normal-forms:0.2.0-devUse CITATION.cff to cite the artifact and preprint. The code is licensed under the Apache License 2.0.