A staged division-free integer determinant

An executable determinant for integer matrices. It runs the stages of Bird's division-free algorithm, but stores every intermediate stage as a dense table of row vectors, so that each stage is computed from the materialized previous one. This is meant to avoid recomputation: Mathlib's BirdDet.birdDet represents each stage as a function whose entries are recomputed recursively, and Matrix.det is a permutation sum. No bound on the number of ring operations is proved here; the result is proved equal to Matrix.det.

Main definitions

• Rational.DeterminantAlgorithm.Table: a dense square integer matrix.
• Rational.DeterminantAlgorithm.denote, Rational.DeterminantAlgorithm.tabulate: conversion between tables and matrices.
• Rational.DeterminantAlgorithm.determinant: the staged determinant.

Main results

• Rational.DeterminantAlgorithm.determinant_eq: the staged determinant is Matrix.det.

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/Determinant.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.
• The shared bridge lemmas in Complexity/Computability/Circuit/Bird.lean restate lemmas private in Mathlib's development (Mathlib/LinearAlgebra/Matrix/Determinant/Bird/Correctness.lean, Copyright (c) 2026 Paul Cadman, Apache 2.0).

@[reducible, inline]

abbrev Cslib.Circuits.Rational.DeterminantAlgorithm.Table (n : ℕ) : Type

A dense square integer matrix stored as a vector of row vectors.

def Cslib.Circuits.Rational.DeterminantAlgorithm.denote {n : ℕ} (A : Table n) : Matrix (Fin n) (Fin n) ℤ

Read a dense integer table as a matrix.

def Cslib.Circuits.Rational.DeterminantAlgorithm.tabulate {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : Table n

Materialize every entry of an integer matrix into a dense table.

@[simp]

theorem Cslib.Circuits.Rational.DeterminantAlgorithm.denote_tabulate {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : denote (tabulate A) = A

def Cslib.Circuits.Rational.DeterminantAlgorithm.step {n : ℕ} (A F : Table n) : Table n

One division-free Bird determinant stage on stored tables.

def Cslib.Circuits.Rational.DeterminantAlgorithm.stages {n : ℕ} (A : Table n) : ℕ → Table n

Iterate the division-free determinant stage.

theorem Cslib.Circuits.Rational.DeterminantAlgorithm.stages_spec {n : ℕ} (A : Table n) (k : ℕ) : denote (stages A k) = (BirdDet.Spec.stepEntry (denote A))^[k] (denote A)

def Cslib.Circuits.Rational.DeterminantAlgorithm.determinant {n : ℕ} : Table n → ℤ

Compute the determinant from the final Bird stage, including dimension zero.

Compatibility bridges

The public integer-specialized interfaces are retained. Their proofs use the shared commutative-ring bridges in Complexity/Computability/Circuit/Bird.lean.

theorem Cslib.Circuits.Rational.DeterminantAlgorithm.sumFrom_eq_sum_Ico {n lo : ℕ} (f : ℕ → ℤ) : BirdDet.sumFrom n lo f = ∑ k ∈ Finset.Ico lo n, f k

theorem Cslib.Circuits.Rational.DeterminantAlgorithm.sumFrom_fin_tail {n : ℕ} (i : Fin n) (f : ℕ → ℤ) : BirdDet.sumFrom n (↑i + 1) f = ∑ k > i, f ↑k

theorem Cslib.Circuits.Rational.DeterminantAlgorithm.iterate_array_spec {n : ℕ} (A : Array ℤ) (hA : A.size = n * n) (t : ℕ) (i j : Fin n) : (BirdDet.stepEntry n A)^[t] (BirdDet.get n A) ↑i ↑j = (BirdDet.Spec.stepEntry (Matrix.ofArray A hA))^[t] (Matrix.ofArray A hA) i j

theorem Cslib.Circuits.Rational.DeterminantAlgorithm.array_spec {n : ℕ} (A : Array ℤ) (hA : A.size = n * n) : BirdDet.birdDet n A = BirdDet.Spec.birdDet (Matrix.ofArray A hA)

theorem Cslib.Circuits.Rational.DeterminantAlgorithm.spec_eq_det {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : BirdDet.Spec.birdDet A = A.det

theorem Cslib.Circuits.Rational.DeterminantAlgorithm.determinant_eq {n : ℕ} (A : Table n) : determinant A = (denote A).det

A genuine executable determinant, not Matrix.det's permutation sum.