cff-version: 1.2.0
title: >-
  Machine-Checked Arithmetic Bit Complexity of the Kannan--Bachem Smith
  Normal Form in Lean 4
message: >-
  If you use this artifact, please cite the preprint and software metadata
  below.
type: software
authors:
  - family-names: Ji
    given-names: Junye
    affiliation: University of Washington
license: Apache-2.0
version: 0.2.0-dev
date-released: 2026-08-01
repository-code: https://github.com/JJYYY-JJY/lean-normal-forms
url: https://arxiv.org/abs/2607.22524
abstract: >-
  Lean 4 verification of a value-producing Kannan--Bachem Smith reduction for
  nonsingular square integer matrices. The artifact returns explicit
  two-sided inverse certificates and proves fixed-polynomial bounds for its
  execution-derived binary arithmetic trace and concrete output encoding.
keywords:
  - Lean 4
  - Smith normal form
  - Kannan--Bachem algorithm
  - bit complexity
  - formalized mathematics
preferred-citation:
  type: article
  title: >-
    Machine-Checked Arithmetic Bit Complexity of the Kannan--Bachem Smith
    Normal Form in Lean 4
  authors:
    - family-names: Ji
      given-names: Junye
  year: 2026
  url: https://arxiv.org/abs/2607.22524