Machine-Checked Kannan--Bachem Smith Reduction

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.

Scope

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.

Published endpoint

import NormalForms

#check NormalForms.Research.KannanBachem.VerifiedSmithPolynomialBitCostResult
#check NormalForms.Research.KannanBachem.verifiedSmithPolynomialBitCost

verifiedSmithPolynomialBitCost 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.

Cost model

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.

Verify

The repository pins Lean and mathlib. The complete verification command is:

scripts/verify.sh

It 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-dev

Citation and license

Use CITATION.cff to cite the artifact and preprint. The code is licensed under the Apache License 2.0.