35.13. HexSmith: integer Smith normal form🔗

35.13.1. Introduction🔗

HexSmith computes canonical Smith normal form for rectangular integer matrices. The Mathlib-free executable layer provides a form-only path, a transform-producing path with explicit inverses, an independent certificate checker, invariant factors, system criteria, and abelian-presentation data.

The companion HexSmithMathlib is correspondence-only: it builds Mathlib's Smith-basis and quotient-decomposition structures from the executable output without running a second Smith computation.

35.13.2. Form-only and certified-transform use🔗

Use Hex.Matrix.snf when only the canonical matrix is needed. The projections Hex.Matrix.snfRank and Hex.Matrix.invariantFactors use the same form-only engine and do not accumulate transforms. Use Hex.Matrix.snfData when a change of basis or replayable certificate is required.

def

Hex.Matrix.snf {n m : ℕ} (A : Hex.Matrix ℤ n m) : Hex.Matrix ℤ n m
Hex.Matrix.snf {n m : ℕ}
  (A : Hex.Matrix ℤ n m) :
  Hex.Matrix ℤ n m

The canonical Smith matrix, computed without allocating transforms.

def

Hex.Matrix.snfRank {n m : ℕ} (A : Hex.Matrix ℤ n m) : ℕ
Hex.Matrix.snfRank {n m : ℕ}
  (A : Hex.Matrix ℤ n m) : ℕ

The number of nonzero diagonal entries in snf A.

def

Hex.Matrix.invariantFactors {n m : ℕ} (A : Hex.Matrix ℤ n m) :
  Vector ℤ A.snfRank
Hex.Matrix.invariantFactors {n m : ℕ}
  (A : Hex.Matrix ℤ n m) :
  Vector ℤ A.snfRank

The positive invariant factors in divisibility-chain order.

def

Hex.Matrix.snfData {n m : ℕ} (A : Hex.Matrix ℤ n m) :
  Hex.Matrix.SmithData n m
Hex.Matrix.snfData {n m : ℕ}
  (A : Hex.Matrix ℤ n m) :
  Hex.Matrix.SmithData n m

Smith form together with both transforms and their explicit inverses.

def

Hex.Matrix.snfCert {n m : ℕ} (A : Hex.Matrix ℤ n m)
  (S : Hex.Matrix.SmithData n m) (T : Hex.Matrix ℤ n m) : Bool
Hex.Matrix.snfCert {n m : ℕ}
  (A : Hex.Matrix ℤ n m)
  (S : Hex.Matrix.SmithData n m)
  (T : Hex.Matrix ℤ n m) : Bool

Accept (S,T) as Smith data for A, where T = S.left * A is supplied to keep the checker from allocating either full product internally.

The following code is elaborated with the manual. The input diagonal does not yet form a divisibility chain: the canonical output replaces (6,4) by (2,12).

open Hex Hex.Matrix

namespace HexSmithChapterExample

private def A : Matrix Int 2 2 := #m[6, 0; 0, 4]

#guard snf A == #m[2, 0; 0, 12]
#guard (invariantFactors A).toList == [2, 12]

private def S : SmithData 2 2 := snfData A

#guard S.left * A * S.right == diagMatrix S.diag 2 2
#guard S.left * S.leftInv == Matrix.identity 2
#guard S.right * S.rightInv == Matrix.identity 2
#guard snfCert A S (S.left * A)

end HexSmithChapterExample

Diagonal input has a specialized route that bypasses the classical pivot loop. Its transform-producing counterpart follows the same fixed gcd/lcm network.

def

Hex.Matrix.snfDiagonal {r : ℕ} (d : Vector ℤ r) : Hex.Matrix ℤ r r
Hex.Matrix.snfDiagonal {r : ℕ}
  (d : Vector ℤ r) : Hex.Matrix ℤ r r

Smith form of a diagonal matrix without allocating transforms.

def

Hex.Matrix.snfDiagonalData {r : ℕ} (d : Vector ℤ r) :
  Hex.Matrix.SmithData r r
Hex.Matrix.snfDiagonalData {r : ℕ}
  (d : Vector ℤ r) :
  Hex.Matrix.SmithData r r

Smith data for a diagonal matrix, including both transforms and inverses.

35.13.3. Systems and presentations🔗

The Smith layer characterizes integer solvability by transformed-coordinate divisibility and a trailing-zero condition. The executable coefficient solver is the existing Hermite operation Hex.Matrix.latticeCoeffs; Smith does not duplicate it.

theorem

Hex.Matrix.solvable_iff_dvd {n m : ℕ} {A : Hex.Matrix ℤ n m}
  {S : Hex.Matrix.SmithData n m} (hS : A.IsSNF S) (b : Vector ℤ m) :
  (∃ x, Hex.Matrix.vecMul x A = b) ↔
    (∀ (i : Fin S.rank),
        S.diag[i] ∣ (Hex.Matrix.vecMul b S.right)[⟨↑i, ⋯⟩]) ∧
      ∀ (j : Fin m), S.rank ≤ ↑j → (Hex.Matrix.vecMul b S.right)[j] = 0
Hex.Matrix.solvable_iff_dvd {n m : ℕ}
  {A : Hex.Matrix ℤ n m}
  {S : Hex.Matrix.SmithData n m}
  (hS : A.IsSNF S) (b : Vector ℤ m) :
  (∃ x, Hex.Matrix.vecMul x A = b) ↔
    (∀ (i : Fin S.rank),
        S.diag[i] ∣
          (Hex.Matrix.vecMul b
              S.right)[⟨↑i, ⋯⟩]) ∧
      ∀ (j : Fin m),
        S.rank ≤ ↑j →
          (Hex.Matrix.vecMul b
                S.right)[j] =
            0

Smith solvability is coordinatewise divisibility on the nonzero diagonal, together with vanishing of every trailing transformed coordinate.

def

Hex.Matrix.latticeCoeffs {n m : ℕ} (A : Hex.Matrix ℤ n m)
  (v : Vector ℤ m) : Option (Vector ℤ n)
Hex.Matrix.latticeCoeffs {n m : ℕ}
  (A : Hex.Matrix ℤ n m)
  (v : Vector ℤ m) : Option (Vector ℤ n)

Integer coefficients expressing v as a combination of the rows of A, or none when the forward HNF solve does not verify.

open Hex Hex.Matrix

namespace HexSmithSystemsExample

private def A : Matrix Int 2 2 := #m[2, 0; 0, 6]
private def solvable : Vector Int 2 := #v[4, 18]
private def impossible : Vector Int 2 := #v[1, 0]

#guard (latticeCoeffs A solvable).isSome
#guard !(latticeCoeffs A impossible).isSome

private def presentation : Matrix Int 2 3 :=
  #m[2, 0, 0; 0, 6, 0]

#guard (abelianStructure presentation).freeRank == 1
#guard
  (abelianStructure presentation).torsionFactors == #[2, 6]

end HexSmithSystemsExample

def

Hex.Matrix.abelianStructure {n m : ℕ} (A : Hex.Matrix ℤ n m) :
  Hex.Matrix.AbelianStructure
Hex.Matrix.abelianStructure {n m : ℕ}
  (A : Hex.Matrix ℤ n m) :
  Hex.Matrix.AbelianStructure

The structure of ℤᵐ / rowlattice A: free rank and non-unit torsion invariants, in divisibility-chain order.

theorem

Hex.Matrix.abelianStructure_torsionFactors {n m : ℕ}
  (A : Hex.Matrix ℤ n m) :
  A.abelianStructure.torsionFactors =
    (List.filterMap (fun d => if 1 < d then some d.natAbs else none)
        A.invariantFactors.toList).toArray
Hex.Matrix.abelianStructure_torsionFactors
  {n m : ℕ} (A : Hex.Matrix ℤ n m) :
  A.abelianStructure.torsionFactors =
    (List.filterMap
        (fun d =>
          if 1 < d then some d.natAbs
          else none)
        A.invariantFactors.toList).toArray

The torsion factors are exactly the non-unit invariant factors, converted to natural numbers in divisibility-chain order.

def

Hex.Matrix.smithBasis {n m : ℕ} (A : Hex.Matrix ℤ n m) :
  Hex.Matrix ℤ A.snfRank m
Hex.Matrix.smithBasis {n m : ℕ}
  (A : Hex.Matrix ℤ n m) :
  Hex.Matrix ℤ A.snfRank m

The independent relation rows obtained by discarding the zero rows of the Smith-transformed presentation.

35.13.4. Determinantal divisors and uniqueness🔗

Hex.Matrix.detDivisor is defined independently as the gcd of all minors of a fixed size. The Smith contract identifies it with the product of the leading invariant factors; comparing those products proves that any two valid Smith data records have the same rank, invariant factors, and form.

def

Hex.Matrix.detDivisor {n m : ℕ} (A : Hex.Matrix ℤ n m) (k : ℕ) : ℕ
Hex.Matrix.detDivisor {n m : ℕ}
  (A : Hex.Matrix ℤ n m) (k : ℕ) : ℕ

The natural gcd of the determinants of all k × k minors. Row and column selections are enumerated in the canonical strictly increasing order provided by selectedColumnTuples; the definition therefore contains no reference to snf. The empty minor has determinant one.

Direct evaluation enumerates all k × k minors and is exponential in the matrix dimensions. This is a specification surface for uniqueness proofs, not the executable way to obtain invariant factors; use invariantFactors for computation.

theorem

Hex.Matrix.IsSNF.detDivisor_eq {n m : ℕ} {A : Hex.Matrix ℤ n m}
  {S : Hex.Matrix.SmithData n m} (h : A.IsSNF S) (k : ℕ) :
  A.detDivisor k =
    if k ≤ S.rank then
      (Vector.foldl (fun x1 x2 => x1 * x2) 1 (S.diag.take k)).natAbs
    else 0
Hex.Matrix.IsSNF.detDivisor_eq {n m : ℕ}
  {A : Hex.Matrix ℤ n m}
  {S : Hex.Matrix.SmithData n m}
  (h : A.IsSNF S) (k : ℕ) :
  A.detDivisor k =
    if k ≤ S.rank then
      (Vector.foldl (fun x1 x2 => x1 * x2)
          1 (S.diag.take k)).natAbs
    else 0

Determinantal divisors characterize every Smith form: within the rank they are prefix products of the invariant factors, and above the rank they vanish.

theorem

Hex.Matrix.IsSNF.rank_eq {n m : ℕ} {A : Hex.Matrix ℤ n m}
  {S S' : Hex.Matrix.SmithData n m} (h : A.IsSNF S) (h' : A.IsSNF S') :
  S.rank = S'.rank
Hex.Matrix.IsSNF.rank_eq {n m : ℕ}
  {A : Hex.Matrix ℤ n m}
  {S S' : Hex.Matrix.SmithData n m}
  (h : A.IsSNF S) (h' : A.IsSNF S') :
  S.rank = S'.rank

Any two Smith witnesses for the same matrix have the same rank.

theorem

Hex.Matrix.IsSNF.diag_eq {n m : ℕ} {A : Hex.Matrix ℤ n m}
  {S S' : Hex.Matrix.SmithData n m} (h : A.IsSNF S) (h' : A.IsSNF S')
  (i : ℕ) (hi : i < S.rank) (hi' : i < S'.rank) : S.diag[i] = S'.diag[i]
Hex.Matrix.IsSNF.diag_eq {n m : ℕ}
  {A : Hex.Matrix ℤ n m}
  {S S' : Hex.Matrix.SmithData n m}
  (h : A.IsSNF S) (h' : A.IsSNF S')
  (i : ℕ) (hi : i < S.rank)
  (hi' : i < S'.rank) :
  S.diag[i] = S'.diag[i]

Any two Smith witnesses have the same invariant factor at every valid index. The two bounds are kept explicit so callers do not need to transport dependent Fin values across rank_eq.

open Hex Hex.Matrix

namespace HexSmithUniquenessExample

example (A : Matrix Int 2 2) :
    detDivisor A 1 =
      if 1 ≤ (snfData A).rank then
        (((snfData A).diag.take 1).foldl (· * ·) 1).natAbs
      else 0 :=
  (snfData_isSNF A).detDivisor_eq 1

example {A : Matrix Int 2 2} {S T : SmithData 2 2}
    (hS : IsSNF A S) (hT : IsSNF A T) :
    diagMatrix S.diag 2 2 = diagMatrix T.diag 2 2 :=
  hS.form_eq hT

end HexSmithUniquenessExample

35.13.5. Failure and complexity guidance🔗

snf, snfRank, and invariantFactors are total. A failed latticeCoeffs result means no verified coefficient vector was found; completeness says it returns some whenever an integer solution exists. A false snfCert result means only that the supplied data failed replay and must not be trusted; Hex.Matrix.snfCert_sound is the acceptance boundary.

The general implementation is the classical pivot loop. Its declared matrix operation model is cubic, while integer coefficient growth is tracked separately in the committed performance report. snfDiagonal uses a quadratic fixed network and has a measured, growing advantage over routing the same input through general elimination. Transform-producing calls cost more because they maintain four dense matrices.

Do not evaluate detDivisor to compute invariants on nontrivial matrices: it enumerates exponentially many minors. Compute Hex.Matrix.invariantFactors and use Hex.Matrix.IsSNF.detDivisor_eq to reason about the result.

35.13.6. The Mathlib correspondence🔗

The bridge realizes the executable right inverse as an ambient basis and the independent left-transformed relation rows as a basis of the row span.

def

HexSmithMathlib.ambientBasis {n m : ℕ} (A : Hex.Matrix ℤ n m) :
  Module.Basis (Fin m) ℤ (Fin m → ℤ)
HexSmithMathlib.ambientBasis {n m : ℕ}
  (A : Hex.Matrix ℤ n m) :
  Module.Basis (Fin m) ℤ (Fin m → ℤ)

Ambient Smith basis: the rows of the recorded right inverse.

def

HexSmithMathlib.relationBasis {n m : ℕ} (A : Hex.Matrix ℤ n m) :
  Module.Basis (Fin A.snfRank) ℤ ↥(HexSmithMathlib.rowSpan A)
HexSmithMathlib.relationBasis {n m : ℕ}
  (A : Hex.Matrix ℤ n m) :
  Module.Basis (Fin A.snfRank) ℤ
    ↥(HexSmithMathlib.rowSpan A)

The independent Smith relation rows form a basis of the original row span.

These bases and the executable invariant factors construct Mathlib's simultaneous Smith-normal-form structure. The separate chain theorem restores the canonical order not stored in that structure.

def

HexSmithMathlib.smithNormalForm {n m : ℕ} (A : Hex.Matrix ℤ n m) :
  Module.Basis.SmithNormalForm (HexSmithMathlib.rowSpan A) (Fin m)
    A.snfRank
HexSmithMathlib.smithNormalForm {n m : ℕ}
  (A : Hex.Matrix ℤ n m) :
  Module.Basis.SmithNormalForm
    (HexSmithMathlib.rowSpan A) (Fin m)
    A.snfRank

The executable Smith normal form as Mathlib's simultaneous-basis structure for the submodule spanned by the rows.

theorem

HexSmithMathlib.smithNormalForm_chain {n m : ℕ} (A : Hex.Matrix ℤ n m)
  (i : ℕ) (h : i + 1 < A.snfRank) :
  (HexSmithMathlib.smithNormalForm A).a ⟨i, ⋯⟩ ∣
    (HexSmithMathlib.smithNormalForm A).a ⟨i + 1, h⟩
HexSmithMathlib.smithNormalForm_chain
  {n m : ℕ} (A : Hex.Matrix ℤ n m) (i : ℕ)
  (h : i + 1 < A.snfRank) :
  (HexSmithMathlib.smithNormalForm A).a
      ⟨i, ⋯⟩ ∣
    (HexSmithMathlib.smithNormalForm A).a
      ⟨i + 1, h⟩

Consecutive coefficients of the executable Mathlib Smith basis form a divisibility chain.

Finally, the quotient equivalence separates free coordinates from cyclic torsion factors, again using the same executable invariant factors.

def

HexSmithMathlib.quotientEquiv {n m : ℕ} (A : Hex.Matrix ℤ n m) :
  ((Fin m → ℤ) ⧸ HexSmithMathlib.rowSpan A) ≃ₗ[ℤ]
    (Fin (m - A.snfRank) → ℤ) ×
      DirectSum (Fin A.snfRank) fun i =>
        ℤ ⧸ Ideal.span {A.invariantFactors[i]}
HexSmithMathlib.quotientEquiv {n m : ℕ}
  (A : Hex.Matrix ℤ n m) :
  ((Fin m → ℤ) ⧸
      HexSmithMathlib.rowSpan A) ≃ₗ[ℤ]
    (Fin (m - A.snfRank) → ℤ) ×
      DirectSum (Fin A.snfRank) fun i =>
        ℤ ⧸
          Ideal.span
            {A.invariantFactors[i]}

The cokernel of an integer matrix is the direct product of its free part and the cyclic factors computed by the executable Smith algorithm.

35.13.7. Cross-references🔗

HexSmith uses HexMatrix for matrix operations and HexDeterminant for minors and determinants. The Hermite solver and lattice-index operations are supplied by HexHermite.