A list program for the staged integer determinant

Rational.DeterminantAlgorithm.determinant runs the stages of Bird's division-free determinant on dense tables whose dimension is part of the type. This file restates the same staged algorithm as an ordinary program on lists of rows, Rational.detRows, whose dimension is the number of rows, and certifies that it is computable in polynomial time on multi-tape Turing machines over framed lists of binary sign-magnitude integers (Rational.detRows_polytime). Missing entries read as 0 and extra entries are ignored.

It also bounds the size of every value the program computes. For a d × d input whose entries have absolute value below 2 ^ b, every entry of the k-th stage, and every partial sum and product computed while producing it, has absolute value below 2 ^ (b + k * (1 + d + b)). The bounds are also stated for the bit length Rational.intBits of a sign-magnitude binary encoding, and, following the original development, for the stages of the dense tables.

Main definitions

• Rational.rowEntry: entry (i, j) of a list of rows, 0 when missing.
• Rational.rowsOf: the list of rows of a square matrix.
• Rational.stepRows, Rational.stagesRows: one Bird stage, and the iterated stages.
• Rational.detRows: the staged determinant of a list of rows.
• Rational.intBits: the bit length of a sign-magnitude binary integer.
• Rational.stageTableBound: upper bound on the encoded length of any stage table in the first k Bird stages.

Main results

• Rational.detRows_eq: detRows (rowsOf A) = A.det.
• Rational.detRows_eq_det_ofRows: on any list of rows, detRows is the determinant of the square matrix it denotes, of dimension the number of rows.
• Rational.natAbs_rowEntry_stagesRows_lt, Rational.natAbs_stepEntryRows_lt, Rational.natAbs_traceTerms_take_sum_lt, Rational.natAbs_productTerms_take_sum_lt: the size bounds on stage entries and on the partial sums inside one stage.
• Rational.intBits_rowEntry_stagesRows_le: the stage bound in bit length.
• Rational.DeterminantAlgorithm.stages_power_bound: the stage bound for dense tables.
• Rational.length_encList_stagesRows_le: encoded length bound on intermediate stage tables.
• Rational.computableInPolyTime_stagesRows, Rational.detRows_polytime: stagesRows and detRows are computable in polynomial time over encList (encList encIntBin).

References

• The table bounds step_bound, stages_bound and stages_power_bound are adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/Determinant.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

Bounds on the dense table stages

theorem Cslib.Circuits.Rational.DeterminantAlgorithm.step_bound {n : ℕ} (A F : Matrix (Fin n) (Fin n) ℤ) (B C : ℕ) (hA : ∀ (i j : Fin n), |A i j| ≤ ↑B) (hF : ∀ (i j : Fin n), |F i j| ≤ ↑C) (i j : Fin n) : |BirdDet.Spec.stepEntry A F i j| ≤ ↑(2 * n * B * C)

One Bird stage multiplies entry bounds by at most twice the dimension.

theorem Cslib.Circuits.Rational.DeterminantAlgorithm.stages_bound {n : ℕ} (A : Table n) (B : ℕ) (hA : ∀ (i j : Fin n), |denote A i j| ≤ ↑B) (k : ℕ) (i j : Fin n) : |denote (stages A k) i j| ≤ ↑(B * (2 * n * B) ^ k)

Every stored table entry has only linearly many multiplicative growth stages.

theorem Cslib.Circuits.Rational.DeterminantAlgorithm.stages_power_bound {n : ℕ} (A : Table n) (b : ℕ) (hA : ∀ (i j : Fin n), |denote A i j| ≤ 2 ^ b) (k : ℕ) (i j : Fin n) : |denote (stages A k) i j| ≤ 2 ^ (b + k * (1 + n + b))

Binary exponent bound for all stored intermediate tables, including singular inputs.

The list program

def Cslib.Circuits.Rational.rowEntry (rows : List (List ℤ)) (i j : ℕ) : ℤ

Entry (i, j) of a matrix stored as a list of rows; missing entries read as 0.

def Cslib.Circuits.Rational.tabulateRows (d : ℕ) (g : ℕ → ℕ → ℤ) : List (List ℤ)

The d × d list of rows whose entry (i, j) is g i j.

def Cslib.Circuits.Rational.rowsOf {d : ℕ} (A : Matrix (Fin d) (Fin d) ℤ) : List (List ℤ)

The list of rows of a square matrix.

def Cslib.Circuits.Rational.ofRows (rows : List (List ℤ)) : Matrix (Fin rows.length) (Fin rows.length) ℤ

The square matrix denoted by a list of rows: its dimension is the number of rows, missing entries are 0 and extra entries are ignored.

def Cslib.Circuits.Rational.squareRows (rows : List (List ℤ)) : List (List ℤ)

Pad or truncate every row to the number of rows.

def Cslib.Circuits.Rational.traceTerms (A F : List (List ℤ)) (i : ℕ) : List ℤ

The diagonal entries F k k for i < k < d, summed in one Bird stage; d is the number of rows of A.

def Cslib.Circuits.Rational.productTerms (A F : List (List ℤ)) (i j : ℕ) : List ℤ

The products F i k * A k j for i < k < d, summed in one Bird stage; d is the number of rows of A.

def Cslib.Circuits.Rational.stepEntryRows (A F : List (List ℤ)) (i j : ℕ) : ℤ

Entry (i, j) of one Bird stage, BirdDet.Spec.stepEntry, on lists of rows.

def Cslib.Circuits.Rational.stepRows (A F : List (List ℤ)) : List (List ℤ)

One Bird stage on lists of rows.

def Cslib.Circuits.Rational.stagesRows (A : List (List ℤ)) (k : ℕ) : List (List ℤ)

The k-th Bird stage, starting from the squared input.

def Cslib.Circuits.Rational.detRows (A : List (List ℤ)) : ℤ

The staged division-free determinant of a list of rows, including dimension zero.

def Cslib.Circuits.Rational.intBits (z : ℤ) : ℕ

The bit length of an integer in a sign-magnitude binary encoding: one sign bit followed by the binary digits of the absolute value.

theorem Cslib.Circuits.Rational.intBits_eq_length_encIntBin (z : ℤ) : intBits z = (Turing.MultiTapeTM.encIntBin z).length

intBits z is the length of the binary sign-magnitude code of z.

Basic lemmas

theorem Cslib.Circuits.Rational.rowEntry_tabulateRows (d : ℕ) (g : ℕ → ℕ → ℤ) (i j : ℕ) : rowEntry (tabulateRows d g) i j = if i < d ∧ j < d then g i j else 0

@[simp]

theorem Cslib.Circuits.Rational.length_rowsOf {d : ℕ} (A : Matrix (Fin d) (Fin d) ℤ) : (rowsOf A).length = d

theorem Cslib.Circuits.Rational.rowEntry_rowsOf {d : ℕ} (A : Matrix (Fin d) (Fin d) ℤ) (i j : Fin d) : rowEntry (rowsOf A) ↑i ↑j = A i j

theorem Cslib.Circuits.Rational.stagesRows_zero (A : List (List ℤ)) : stagesRows A 0 = squareRows A

theorem Cslib.Circuits.Rational.stagesRows_succ (A : List (List ℤ)) (k : ℕ) : stagesRows A (k + 1) = stepRows A (stagesRows A k)

theorem Cslib.Circuits.Rational.sum_map_drop_range (d lo : ℕ) (f : ℕ → ℤ) : (List.map f (List.drop lo (List.range d))).sum = BirdDet.sumFrom d lo f

A tail of a range, summed as a list, is a tail sum over Fin.

theorem Cslib.Circuits.Rational.sum_map_drop_range_fin {d : ℕ} (i : Fin d) (f : ℕ → ℤ) : (List.map f (List.drop (↑i + 1) (List.range d))).sum = ∑ k > i, f ↑k

Correctness

theorem Cslib.Circuits.Rational.rowEntry_stagesRows (A : List (List ℤ)) (k : ℕ) (i j : Fin A.length) : rowEntry (stagesRows A k) ↑i ↑j = (BirdDet.Spec.stepEntry (ofRows A))^[k] (ofRows A) i j

The list stages agree with the Bird stages of the matrix denoted by the input.

theorem Cslib.Circuits.Rational.detRows_eq_det_ofRows (A : List (List ℤ)) : detRows A = (ofRows A).det

On any list of rows, detRows is the determinant of the square matrix it denotes, of dimension the number of rows.

theorem Cslib.Circuits.Rational.detRows_eq_det_of_rowEntry {d : ℕ} {rows : List (List ℤ)} (A : Matrix (Fin d) (Fin d) ℤ) (hd : rows.length = d) (hA : ∀ (i j : Fin d), rowEntry rows ↑i ↑j = A i j) : detRows rows = A.det

detRows computes the determinant of every list of rows that agrees with a square matrix of its length.

theorem Cslib.Circuits.Rational.detRows_eq {d : ℕ} (A : Matrix (Fin d) (Fin d) ℤ) : detRows (rowsOf A) = A.det

The list program computes the determinant.

theorem Cslib.Circuits.Rational.detRows_rowsOf_denote {d : ℕ} (A : DeterminantAlgorithm.Table d) : detRows (rowsOf (DeterminantAlgorithm.denote A)) = DeterminantAlgorithm.determinant A

The list program agrees with the staged determinant on dense tables.

Size bounds

theorem Cslib.Circuits.Rational.natAbs_sum_le {l : List ℤ} {C : ℕ} (h : ∀ x ∈ l, x.natAbs ≤ C) : l.sum.natAbs ≤ l.length * C

theorem Cslib.Circuits.Rational.natAbs_take_sum_le {l : List ℤ} {C : ℕ} (h : ∀ x ∈ l, x.natAbs ≤ C) (m : ℕ) : (List.take m l).sum.natAbs ≤ l.length * C

Every prefix sum of a list is bounded by its length times a bound on its entries.

theorem Cslib.Circuits.Rational.natAbs_take_sum_le_of_length {l : List ℤ} {C m : ℕ} (hl : l.length ≤ m) (h : ∀ x ∈ l, x.natAbs ≤ C) (k : ℕ) : (List.take k l).sum.natAbs ≤ m * C

Every prefix sum and the sum of a list of terms bounded by C are bounded by m * C, where m bounds the length.

theorem Cslib.Circuits.Rational.natAbs_rowEntry_lt {rows : List (List ℤ)} {b : ℕ} (h : ∀ row ∈ rows, ∀ z ∈ row, z.natAbs < 2 ^ b) (i j : ℕ) : (rowEntry rows i j).natAbs < 2 ^ b

Entry bounds hold for every entry index once they hold for every stored entry.

theorem Cslib.Circuits.Rational.exists_rowEntry_eq {rows : List (List ℤ)} {row : List ℤ} {z : ℤ} (hrow : row ∈ rows) (hz : z ∈ row) : ∃ (i : ℕ) (j : ℕ), rowEntry rows i j = z

Every stored entry of a list of rows is one of its indexed entries.

theorem Cslib.Circuits.Rational.length_traceTerms_le (A F : List (List ℤ)) (i : ℕ) : (traceTerms A F i).length ≤ A.length

theorem Cslib.Circuits.Rational.length_productTerms_le (A F : List (List ℤ)) (i j : ℕ) : (productTerms A F i j).length ≤ A.length

theorem Cslib.Circuits.Rational.natAbs_traceTerms_take_sum_lt {A F : List (List ℤ)} {b e : ℕ} (hF : ∀ (i j : ℕ), (rowEntry F i j).natAbs < 2 ^ e) (i m : ℕ) : (List.take m (traceTerms A F i)).sum.natAbs < 2 ^ (e + (1 + A.length + b))

Every prefix sum of the diagonal terms of one stage obeys the next stage's bound.

theorem Cslib.Circuits.Rational.natAbs_productTerms_take_sum_lt {A F : List (List ℤ)} {b e : ℕ} (hA : ∀ (i j : ℕ), (rowEntry A i j).natAbs < 2 ^ b) (hF : ∀ (i j : ℕ), (rowEntry F i j).natAbs < 2 ^ e) (i j m : ℕ) : (List.take m (productTerms A F i j)).sum.natAbs < 2 ^ (e + (1 + A.length + b))

Every prefix sum of the product terms of one stage obeys the next stage's bound.

theorem Cslib.Circuits.Rational.natAbs_traceTerms_sum_mul_lt {A F : List (List ℤ)} {b e : ℕ} (hA : ∀ (i j : ℕ), (rowEntry A i j).natAbs < 2 ^ b) (hF : ∀ (i j : ℕ), (rowEntry F i j).natAbs < 2 ^ e) (i j : ℕ) : ((traceTerms A F i).sum * rowEntry A i j).natAbs < 2 ^ (e + (1 + A.length + b))

The trace product computed in one stage obeys the next stage's bound.

theorem Cslib.Circuits.Rational.natAbs_stepEntryRows_lt {A F : List (List ℤ)} {b e : ℕ} (hA : ∀ (i j : ℕ), (rowEntry A i j).natAbs < 2 ^ b) (hF : ∀ (i j : ℕ), (rowEntry F i j).natAbs < 2 ^ e) (i j : ℕ) : (stepEntryRows A F i j).natAbs < 2 ^ (e + (1 + A.length + b))

One stage multiplies the entry bound by at most 2 ^ (1 + d + b).

theorem Cslib.Circuits.Rational.natAbs_rowEntry_stagesRows_lt {A : List (List ℤ)} {b : ℕ} (hA : ∀ (i j : ℕ), (rowEntry A i j).natAbs < 2 ^ b) (k i j : ℕ) : (rowEntry (stagesRows A k) i j).natAbs < 2 ^ (b + k * (1 + A.length + b))

Every entry of the k-th stage of an input with entries below 2 ^ b in absolute value is below 2 ^ (b + k * (1 + d + b)), where d is the number of rows.

theorem Cslib.Circuits.Rational.natAbs_lt_of_mem_stagesRows {A : List (List ℤ)} {b : ℕ} (hA : ∀ (i j : ℕ), (rowEntry A i j).natAbs < 2 ^ b) (k : ℕ) {row : List ℤ} (hrow : row ∈ stagesRows A k) {z : ℤ} (hz : z ∈ row) : z.natAbs < 2 ^ (b + k * (1 + A.length + b))

The stage bound for every stored entry of a stage.

Bounds in bit length

theorem Cslib.Circuits.Rational.intBits_le_iff (z : ℤ) (e : ℕ) : intBits z ≤ e + 1 ↔ z.natAbs < 2 ^ e

theorem Cslib.Circuits.Rational.one_le_intBits (z : ℤ) : 1 ≤ intBits z

theorem Cslib.Circuits.Rational.intBits_rowEntry_stagesRows_le {A : List (List ℤ)} {b : ℕ} (hA : ∀ (i j : ℕ), intBits (rowEntry A i j) ≤ b + 1) (k i j : ℕ) : intBits (rowEntry (stagesRows A k) i j) ≤ b + k * (1 + A.length + b) + 1

The stage bound in bit length: inputs of at most b + 1 bits give k-th stage entries of at most b + k * (1 + d + b) + 1 bits.

theorem Cslib.Circuits.Rational.intBits_le_of_mem_stagesRows {A : List (List ℤ)} {b : ℕ} (hA : ∀ row ∈ A, ∀ z ∈ row, intBits z ≤ b + 1) (k : ℕ) {row : List ℤ} (hrow : row ∈ stagesRows A k) {z : ℤ} (hz : z ∈ row) : intBits z ≤ b + k * (1 + A.length + b) + 1

The bit-length stage bound for every stored entry of a stage.

theorem Cslib.Circuits.Rational.intBits_step_le {A F : List (List ℤ)} {b e : ℕ} (hA : ∀ (i j : ℕ), intBits (rowEntry A i j) ≤ b + 1) (hF : ∀ (i j : ℕ), intBits (rowEntry F i j) ≤ e + 1) (i j m : ℕ) : intBits (List.take m (traceTerms A F i)).sum ≤ e + (1 + A.length + b) + 1 ∧ intBits (List.take m (productTerms A F i j)).sum ≤ e + (1 + A.length + b) + 1 ∧ intBits ((traceTerms A F i).sum * rowEntry A i j) ≤ e + (1 + A.length + b) + 1 ∧ intBits (stepEntryRows A F i j) ≤ e + (1 + A.length + b) + 1

The bit-length bound on every value computed in one stage: prefix sums of both term lists, the trace product and the new entry.

Polynomial-time certificate

@[simp]

theorem Cslib.Circuits.Rational.length_tabulateRows (d : ℕ) (g : ℕ → ℕ → ℤ) : (tabulateRows d g).length = d

theorem Cslib.Circuits.Rational.length_of_mem_tabulateRows {d : ℕ} {g : ℕ → ℕ → ℤ} {row : List ℤ} (hrow : row ∈ tabulateRows d g) : row.length = d

@[simp]

theorem Cslib.Circuits.Rational.length_stagesRows (A : List (List ℤ)) (k : ℕ) : (stagesRows A k).length = A.length

theorem Cslib.Circuits.Rational.length_of_mem_stagesRows {A : List (List ℤ)} {k : ℕ} {row : List ℤ} (hrow : row ∈ stagesRows A k) : row.length = A.length

theorem Cslib.Circuits.Rational.intBits_le_length_encList {A : List (List ℤ)} {row : List ℤ} (hrow : row ∈ A) {z : ℤ} (hz : z ∈ row) : intBits z ≤ ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) A).length + 1

def Cslib.Circuits.Rational.stageEntryBound (L k : ℕ) : ℕ

Upper bound on the bit length of any entry in the first k Bird stages of a matrix of encoded length L.

def Cslib.Circuits.Rational.stageRowBound (L k : ℕ) : ℕ

Upper bound on the encoded length of any row in the first k Bird stages of a matrix of encoded length L.

def Cslib.Circuits.Rational.stageTableBound (L k : ℕ) : ℕ

Upper bound on the encoded length of any stage table in the first k Bird stages of a matrix of encoded length L.

theorem Cslib.Circuits.Rational.length_encList_stagesRows_le (A : List (List ℤ)) {i k : ℕ} (hik : i ≤ k) : ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (stagesRows A i)).length ≤ stageTableBound ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) A).length k

Every stage table up to stage k has encoded length bounded by stageTableBound.

theorem Cslib.Circuits.Rational.computableInPolyTime_rowEntry {α : Type} {encIn : α ↪ List Bool} {rows : α → List (List ℤ)} {i j : α → ℕ} (hrows : Turing.MultiTapeTM.ComputableInPolyTime rows encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hi : Turing.MultiTapeTM.ComputableInPolyTime i encIn Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime j encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => rowEntry (rows x) (i x) (j x)) encIn Turing.MultiTapeTM.encIntBin

Matrix entry lookup on a list of rows is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_tabulateRows {α : Type} {encIn : α ↪ List Bool} {d : α → ℕ} {g : α → ℕ → ℕ → ℤ} (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn Turing.MultiTapeTM.encUnary) (hg : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (α × ℕ) × ℕ) => g p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encIn Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encIntBin) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => tabulateRows (d x) (g x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Tabulating a d × d matrix of binary integers from a unary dimension is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_squareRows : Turing.MultiTapeTM.ComputableInPolyTime squareRows (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Padding or truncating a list of rows to a square table is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_traceTerms {α : Type} {encIn : α ↪ List Bool} {A F : α → List (List ℤ)} {i : α → ℕ} (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hF : Turing.MultiTapeTM.ComputableInPolyTime F encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hi : Turing.MultiTapeTM.ComputableInPolyTime i encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => traceTerms (A x) (F x) (i x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Computing the diagonal terms summed in one Bird stage is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_productTerms {α : Type} {encIn : α ↪ List Bool} {A F : α → List (List ℤ)} {i j : α → ℕ} (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hF : Turing.MultiTapeTM.ComputableInPolyTime F encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hi : Turing.MultiTapeTM.ComputableInPolyTime i encIn Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime j encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => productTerms (A x) (F x) (i x) (j x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Computing the product terms summed in one Bird stage is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_stepEntryRows {α : Type} {encIn : α ↪ List Bool} {A F : α → List (List ℤ)} {i j : α → ℕ} (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hF : Turing.MultiTapeTM.ComputableInPolyTime F encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hi : Turing.MultiTapeTM.ComputableInPolyTime i encIn Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime j encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => stepEntryRows (A x) (F x) (i x) (j x)) encIn Turing.MultiTapeTM.encIntBin

Computing one entry of a Bird stage is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_stepRows : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List (List ℤ) × List (List ℤ)) => stepRows p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

One Bird stage on lists of rows is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_stagesRows {α : Type} {encIn : α ↪ List Bool} {A : α → List (List ℤ)} {k : α → ℕ} (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hk : Turing.MultiTapeTM.ComputableInPolyTime k encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => stagesRows (A x) (k x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Iterating k Bird stages on a list of rows is polynomial-time for a unary stage count k.

theorem Cslib.Circuits.Rational.detRows_eq_ite (A : List (List ℤ)) : detRows A = if A.isEmpty = true then 1 else (-1) ^ (A.length - 1) * rowEntry (stagesRows A (A.length - 1)) 0 0

theorem Cslib.Circuits.Rational.detRows_polytime : Turing.MultiTapeTM.ComputableInPolyTime detRows (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) Turing.MultiTapeTM.encIntBin

The staged division-free integer determinant detRows is computable in polynomial time on lists of rows of binary sign-magnitude integers.