Correctness of Bird's determinant algorithm

This file contains a proof that Bird's division-free algorithm computes Matrix.det, in both its matrix form BirdDet.Spec.birdDet (birdDetSpec_eq_det) and its flat-array form BirdDet.birdDet (det_eq_birdDet), formalizing the combinatorial argument of [Richard S. Bird, A simple division-free algorithm for computing determinants][bird2011].

Correspondence with the paper

• A word of length p is a tuple Fin p → Fin n, using the indexing convention above (NB: Indices in Bird's paper start at 1).
• f[α, β], the minor on rows α and columns β, is (A.submatrix α β).det.
• f[iα, jα], a bordered minor, is bminor A i j α, with the word iα spelled Fin.cons i α.
• f[α, α], a principal minor, is pminor A α.
• If i : Fin n represents Bird's symbol r = i.val + 1, then Bird's βᵣ = [r + 1, ..., n] is represented by Finset.Ioi i.
• Bird's Sₚ(βᵣ), the length p subsequences of βᵣ, is represented by S p i.

The theorem names paper_eq1, ..., paper_eq5 follow Bird's numbering.

Main results

• BirdDet.birdDetSpec_eq_det: Matrix.det computes the same determinant as BirdDet.Spec.birdDet
• BirdDet.det_eq_birdDet: Matrix.det computes the same determinant as BirdDet.birdDet

Decomposition S_{p+1}(βᵢ) = { kα | k ∈ βᵢ, α ∈ S_p(β_k) }

Equations (2) and (3): substituting the induction hypothesis

Equation (5): first-column Laplace expansion

Comparing equations (3) and (5): reindex by sorted insert/delete

Bird's Equation (1)

instantiating equation (1) to prove Theorem 1

theorem BirdDet.det_eq_birdDet {R : Type u_1} [CommRing R] {n : ℕ} (A : Array R) (hA : A.size = n * n) : (Matrix.ofArray A hA).det = birdDet n A

BirdDet.birdDet n A computes the determinant of the n × n matrix whose entries are stored in row-major order in A.