Shared correctness bridges for Bird's determinant algorithm

These commutative-ring bridges connect the flat-array implementation and the matrix specification of Bird's division-free algorithm. They form a lightweight shared dependency of the integer staged algorithm and the arithmetic-circuit synthesis, without importing either client hierarchy. No algorithm or resource bound is introduced here.

Main results

• Cslib.Circuits.Bird.sumFrom_eq_sum_Ico, Cslib.Circuits.Bird.sumFrom_fin_tail: suffix sums.
• Cslib.Circuits.Bird.iterate_array_spec, Cslib.Circuits.Bird.array_spec: array/matrix bridges.
• Cslib.Circuits.Bird.spec_eq_det: the matrix specification computes the determinant.

References

• R. S. Bird, A simple division-free algorithm for computing determinants.
• The proofs restate private declarations from Paul Cadman's Mathlib module Mathlib/LinearAlgebra/Matrix/Determinant/Bird/Correctness.lean (Copyright 2026, Apache 2.0). They consolidate the local generic-ring and integer restatements previously in Complexity/Computability/Circuit/Arithmetic/Determinant.lean and Complexity/Computability/Circuit/Rational/Determinant.lean.
• The integer restatement came from OpenAI's formalization [OAI26a], revision adc7f1241b42e322a6451854ab7e4b4c146bf78a, via the complexitylib port [Sch26d], revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

theorem Cslib.Circuits.Bird.sumFrom_eq_sum_Ico {R : Type u_1} [CommRing R] {n lo : ℕ} (f : ℕ → R) : BirdDet.sumFrom n lo f = ∑ k ∈ Finset.Ico lo n, f k

The recursive suffix sum is the sum over a natural-number interval.

theorem Cslib.Circuits.Bird.sumFrom_fin_tail {R : Type u_1} [CommRing R] {n : ℕ} (i : Fin n) (f : ℕ → R) : BirdDet.sumFrom n (↑i + 1) f = ∑ k > i, f ↑k

A suffix starting after a finite index is the sum over its strict upper interval.

theorem Cslib.Circuits.Bird.iterate_array_spec {R : Type u_1} [CommRing R] {n : ℕ} (A : Array R) (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

Iterated flat-array stages agree with iterated matrix stages.

theorem Cslib.Circuits.Bird.array_spec {R : Type u_1} [CommRing R] {n : ℕ} (A : Array R) (hA : A.size = n * n) : BirdDet.birdDet n A = BirdDet.Spec.birdDet (Matrix.ofArray A hA)

The flat-array determinant agrees with the matrix specification, including dimension zero.

theorem Cslib.Circuits.Bird.spec_eq_det {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) : BirdDet.Spec.birdDet A = A.det

Bird's matrix specification computes the determinant over every commutative ring.