Correctness of the effective binary basis construction

def MIPRE.LowDegree.BinaryLinear.typedInsert {n t : ℕ} (b : List (Pivot n t)) (r : Row n t) : List (Pivot n t)

The program's pivot choice, applied to typed coordinate vectors.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LowDegree.BinaryLinear.vector_eq_zero_of_firstOne_ge {n : ℕ} (v : Fin n → ZMod 2) (h : ¬firstOne (vectorBits v) < n) : v = 0

theorem MIPRE.LowDegree.BinaryLinear.firstOne_vectorBits_one {n : ℕ} (v : Fin n → ZMod 2) (h : firstOne (vectorBits v) < n) : v ⟨firstOne (vectorBits v), h⟩ = 1

theorem MIPRE.LowDegree.BinaryLinear.insertRow_pivotBits {n t : ℕ} (b : List (Pivot n t)) (r : Row n t) : insertRow (List.map pivotBits b) (rowBits r) = List.map pivotBits (typedInsert b r)

Raw row insertion uses exactly the verified typed pivot rule.

theorem MIPRE.LowDegree.BinaryLinear.IsPivotBasis.typedInsert {n t : ℕ} {b : List (Pivot n t)} (hb : IsPivotBasis b) (r : Row n t) : IsPivotBasis (BinaryLinear.typedInsert b r)

Insertion maintains the triangular pivot invariant.

def MIPRE.LowDegree.BinaryLinear.typedBasis {n t : ℕ} (rows : List (Row n t)) : List (Pivot n t)

Forward elimination, with its vectors and coefficient certificates retained.

Equations

• MIPRE.LowDegree.BinaryLinear.typedBasis rows = List.foldl MIPRE.LowDegree.BinaryLinear.typedInsert [] rows

theorem MIPRE.LowDegree.BinaryLinear.fold_insertRow_pivotBits {n t : ℕ} (rows : List (Row n t)) (b : List (Pivot n t)) : List.foldl insertRow (List.map pivotBits b) (List.map rowBits rows) = List.map pivotBits (List.foldl typedInsert b rows)

theorem MIPRE.LowDegree.BinaryLinear.basisRowsProg_correct {n t : ℕ} (rows : List (Row n t)) : basisRowsProg.toFun (List.map rowBits rows) = List.map pivotBits (typedBasis rows)

The actual ambient program constructs precisely the typed binary basis.

theorem MIPRE.LowDegree.BinaryLinear.fold_typedInsert_isPivotBasis {n t : ℕ} (rows : List (Row n t)) (b : List (Pivot n t)) (hb : IsPivotBasis b) : IsPivotBasis (List.foldl typedInsert b rows)

theorem MIPRE.LowDegree.BinaryLinear.typedBasis_isPivotBasis {n t : ℕ} (rows : List (Row n t)) : IsPivotBasis (typedBasis rows)

theorem MIPRE.LowDegree.BinaryLinear.typedBasis_linearIndependent {n t : ℕ} (rows : List (Row n t)) : LinearIndependent (ZMod 2) (pivotVectors (typedBasis rows))

theorem MIPRE.LowDegree.BinaryLinear.typedBasis_length_le {n t : ℕ} (rows : List (Row n t)) : (typedBasis rows).length ≤ n

theorem MIPRE.LowDegree.BinaryLinear.typedReduceStep_mem_iff {n t : ℕ} (S : Submodule (ZMod 2) (Fin n → ZMod 2)) (r : Row n t) (p : Pivot n t) (hp : p.2.1 ∈ S) : (typedReduceStep r p).1 ∈ S ↔ r.1 ∈ S

Adding a stored vector preserves membership in every subspace containing it.

theorem MIPRE.LowDegree.BinaryLinear.typedReduce_mem_iff {n t : ℕ} (S : Submodule (ZMod 2) (Fin n → ZMod 2)) (b : List (Pivot n t)) (r : Row n t) (hb : ∀ p ∈ b, p.2.1 ∈ S) : (typedReduce b r).1 ∈ S ↔ r.1 ∈ S

theorem MIPRE.LowDegree.BinaryLinear.typedInsert_mem_iff {n t : ℕ} (S : Submodule (ZMod 2) (Fin n → ZMod 2)) (b : List (Pivot n t)) (r : Row n t) : (∀ p ∈ typedInsert b r, p.2.1 ∈ S) ↔ (∀ p ∈ b, p.2.1 ∈ S) ∧ r.1 ∈ S

Insertion preserves exactly the subspace generated by the old basis and new row.

theorem MIPRE.LowDegree.BinaryLinear.fold_typedInsert_mem_iff {n t : ℕ} (S : Submodule (ZMod 2) (Fin n → ZMod 2)) (rows : List (Row n t)) (b : List (Pivot n t)) : (∀ p ∈ List.foldl typedInsert b rows, p.2.1 ∈ S) ↔ (∀ p ∈ b, p.2.1 ∈ S) ∧ ∀ r ∈ rows, r.1 ∈ S

theorem MIPRE.LowDegree.BinaryLinear.typedBasis_mem_iff {n t : ℕ} (S : Submodule (ZMod 2) (Fin n → ZMod 2)) (rows : List (Row n t)) : (∀ p ∈ typedBasis rows, p.2.1 ∈ S) ↔ ∀ r ∈ rows, r.1 ∈ S

Output and input generate exactly the same binary subspace.

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

Equations

• MIPRE.LowDegree.BinaryLinear.pivotSpan b = Submodule.span (ZMod 2) {v : Fin n → ZMod 2 | ∃ p ∈ b, p.2.1 = v}

def MIPRE.LowDegree.BinaryLinear.rowSpan {n t : ℕ} (rows : List (Row n t)) : Submodule (ZMod 2) (Fin n → ZMod 2)

Equations

• MIPRE.LowDegree.BinaryLinear.rowSpan rows = Submodule.span (ZMod 2) {v : Fin n → ZMod 2 | ∃ r ∈ rows, r.1 = v}

theorem MIPRE.LowDegree.BinaryLinear.typedBasis_span {n t : ℕ} (rows : List (Row n t)) : pivotSpan (typedBasis rows) = rowSpan rows

The constructed independent vectors span the original family.