Verified canonical binary elimination for auxiliary dual checks

The effective elimination library chooses the first nonzero coordinate at each insertion. Its resulting pivot set is exactly the dimension-defined canonical pivot set used by CL.canonLin. Thus its residual, not merely an arbitrary equivalent quotient representative, computes that canonical map.

theorem MIPRE.Introspection.AuxiliaryCanonical.firstOne_before (bs : Cost.BitStr) (j : ℕ) (hj : j < LowDegree.BinaryLinear.firstOne bs) : List.getD bs j false = false

theorem MIPRE.Introspection.AuxiliaryCanonical.firstOne_vector_before {n : ℕ} (v : Fin n → ZMod 2) (i : Fin n) (hi : ↑i < LowDegree.BinaryLinear.firstOne (LowDegree.BinaryLinear.vectorBits v)) : v i = 0

def MIPRE.Introspection.AuxiliaryCanonical.Leading {n t : ℕ} (b : List (LowDegree.BinaryLinear.Pivot n t)) : Prop

Equations

• MIPRE.Introspection.AuxiliaryCanonical.Leading b = ∀ p ∈ b, ∀ i < p.1, p.2.1 i = 0

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

theorem MIPRE.Introspection.AuxiliaryCanonical.typedBasis_leading {n t : ℕ} (rows : List (LowDegree.BinaryLinear.Row n t)) : Leading (LowDegree.BinaryLinear.typedBasis rows)

theorem MIPRE.Introspection.AuxiliaryCanonical.pivot_one {n t : ℕ} {b : List (LowDegree.BinaryLinear.Pivot n t)} (hb : LowDegree.BinaryLinear.IsPivotBasis b) (p : LowDegree.BinaryLinear.Pivot n t) (hp : p ∈ b) : p.2.1 p.1 = 1

theorem MIPRE.Introspection.AuxiliaryCanonical.pivot_nodup {n t : ℕ} {b : List (LowDegree.BinaryLinear.Pivot n t)} (hb : LowDegree.BinaryLinear.IsPivotBasis b) : (List.map Prod.fst b).Nodup

theorem MIPRE.Introspection.AuxiliaryCanonical.pivotSpan_range {n t : ℕ} (b : List (LowDegree.BinaryLinear.Pivot n t)) : LowDegree.BinaryLinear.pivotSpan b = Submodule.span (ZMod 2) (Set.range (LowDegree.BinaryLinear.pivotVectors b))

theorem MIPRE.Introspection.AuxiliaryCanonical.finrank_pivotSpan {n t : ℕ} {b : List (LowDegree.BinaryLinear.Pivot n t)} (hb : LowDegree.BinaryLinear.IsPivotBasis b) : Module.finrank (ZMod 2) ↥(LowDegree.BinaryLinear.pivotSpan b) = b.length

theorem MIPRE.Introspection.AuxiliaryCanonical.leading_mem_pivots {n : ℕ} (S : Submodule (ZMod 2) (Fin n → ZMod 2)) (v : Fin n → ZMod 2) (hv : v ∈ S) (j : Fin n) (hj : v j ≠ 0) (hprev : ∀ i < j, v i = 0) : j ∈ CL.pivots S

A leading nonzero coordinate of a subspace vector is a canonical pivot.

theorem MIPRE.Introspection.AuxiliaryCanonical.pivot_set_canonical {n t : ℕ} {b : List (LowDegree.BinaryLinear.Pivot n t)} (hb : LowDegree.BinaryLinear.IsPivotBasis b) (hl : Leading b) : (List.map Prod.fst b).toFinset = CL.pivots (LowDegree.BinaryLinear.pivotSpan b)

The program's stored pivot indices equal the source's canonical pivot set.

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

theorem MIPRE.Introspection.AuxiliaryCanonical.typedReduce_canonLin {n t : ℕ} {b : List (LowDegree.BinaryLinear.Pivot n t)} (hb : LowDegree.BinaryLinear.IsPivotBasis b) (hl : Leading b) (r : LowDegree.BinaryLinear.Row n t) : (LowDegree.BinaryLinear.typedReduce b r).1 = (CL.canonLin (LowDegree.BinaryLinear.pivotSpan b)) r.1

theorem MIPRE.Introspection.AuxiliaryCanonical.typedBasis_canonLin {n t : ℕ} (rows : List (LowDegree.BinaryLinear.Row n t)) (v : Fin n → ZMod 2) : (LowDegree.BinaryLinear.typedReduce (LowDegree.BinaryLinear.typedBasis rows) (v, 0)).1 = (CL.canonLin (LowDegree.BinaryLinear.rowSpan rows)) v

Canonical reduction for an arbitrary finite generating family.

noncomputable def MIPRE.Introspection.AuxiliaryCanonical.canonicalProg : Cost.PolyTimeFun (List Cost.BitStr × Cost.BitStr) Cost.BitStr

A single uniform polynomial-time program for the exact canonical quotient representative. The coefficient width is zero, since no certificate is output.

Equations

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

theorem MIPRE.Introspection.AuxiliaryCanonical.canonicalProg_correct {n : ℕ} (vs : List (Fin n → ZMod 2)) (v : Fin n → ZMod 2) : canonicalProg.toFun (List.map LowDegree.BinaryLinear.vectorBits vs, LowDegree.BinaryLinear.vectorBits v) = LowDegree.BinaryLinear.vectorBits ((CL.canonLin (Submodule.span (ZMod 2) {x : Fin n → ZMod 2 | x ∈ vs})) v)