Triangular pivot bases and certified binary reduction

theorem MIPRE.LowDegree.BinaryLinear.instFactPrimeOfNatNat_mIPRE : Fact (Nat.Prime 2)

def MIPRE.LowDegree.BinaryLinear.IsPivotBasis {n t : ℕ} : List (Pivot n t) → Prop

In insertion order, each row has pivot one and every later row vanishes at that pivot. Pivots need not be numerically ordered.

Equations

• MIPRE.LowDegree.BinaryLinear.IsPivotBasis [] = True
• MIPRE.LowDegree.BinaryLinear.IsPivotBasis (p :: b) = (p.2.1 p.1 = 1 ∧ (∀ q ∈ b, q.2.1 p.1 = 0) ∧ MIPRE.LowDegree.BinaryLinear.IsPivotBasis b)

theorem MIPRE.LowDegree.BinaryLinear.binary_eq_zero_or_one (x : ZMod 2) : x = 0 ∨ x = 1

theorem MIPRE.LowDegree.BinaryLinear.typedReduceStep_pivot_zero {n t : ℕ} (r : Row n t) (p : Pivot n t) (hp : p.2.1 p.1 = 1) : (typedReduceStep r p).1 p.1 = 0

theorem MIPRE.LowDegree.BinaryLinear.typedReduceStep_preserves_zero {n t : ℕ} (r : Row n t) (p : Pivot n t) (j : Fin n) (hr : r.1 j = 0) (hp : p.2.1 j = 0) : (typedReduceStep r p).1 j = 0

theorem MIPRE.LowDegree.BinaryLinear.typedReduce_preserves_zero {n t : ℕ} (b : List (Pivot n t)) (r : Row n t) (j : Fin n) (hr : r.1 j = 0) (hb : ∀ p ∈ b, p.2.1 j = 0) : (typedReduce b r).1 j = 0

theorem MIPRE.LowDegree.BinaryLinear.typedReduce_pivots_zero {n t : ℕ} (b : List (Pivot n t)) (hb : IsPivotBasis b) (r : Row n t) (p : Pivot n t) : p ∈ b → (typedReduce b r).1 p.1 = 0

Reducing against a triangular basis zeros all of its pivot coordinates.

theorem MIPRE.LowDegree.BinaryLinear.IsPivotBasis.append_reduced {n t : ℕ} {b : List (Pivot n t)} (hb : IsPivotBasis b) (r : Row n t) (j : Fin n) (hj : (typedReduce b r).1 j = 1) : IsPivotBasis (b ++ [(j, typedReduce b r)])

A reduced nonzero row can be appended at any of its nonzero coordinates.

def MIPRE.LowDegree.BinaryLinear.pivotVectors {n t : ℕ} (b : List (Pivot n t)) : Fin b.length → Fin n → ZMod 2

The vector family extracted in insertion order.

Equations

• MIPRE.LowDegree.BinaryLinear.pivotVectors b i = b[i].2.1

theorem MIPRE.LowDegree.BinaryLinear.pivotVectors_cons {n t : ℕ} (p : Pivot n t) (b : List (Pivot n t)) : pivotVectors (p :: b) = Fin.cons p.2.1 (pivotVectors b)

theorem MIPRE.LowDegree.BinaryLinear.IsPivotBasis.linearIndependent {n t : ℕ} {b : List (Pivot n t)} (hb : IsPivotBasis b) : LinearIndependent (ZMod 2) (pivotVectors b)

Triangular pivots certify linear independence of the stored vectors.

theorem MIPRE.LowDegree.BinaryLinear.IsPivotBasis.length_le {n t : ℕ} {b : List (Pivot n t)} (hb : IsPivotBasis b) : b.length ≤ n

A pivot basis contains at most the ambient dimension many rows.