Documentation

MIPRE.Foundations.LowDegree.BinarySolve

Solving binary linear systems with certified elimination #

source
@[simp]
theorem MIPRE.LowDegree.BinaryLinear.pivotSpan_nil {n t : ℕ} :
pivotSpan [] = ⊥
source
theorem MIPRE.LowDegree.BinaryLinear.pivotSpan_cons {n t : ℕ} (p : Pivot n t) (b : List (Pivot n t)) :
pivotSpan (p :: b) = ZMod 2 ∙ p.2.1 ⊔ pivotSpan b
source
theorem MIPRE.LowDegree.BinaryLinear.IsPivotBasis.eq_zero_of_pivots_zero {n t : ℕ} {b : List (Pivot n t)} (hb : IsPivotBasis b) (v : Fin n → ZMod 2) (hv : v ∈ pivotSpan b) (hz : ∀ p ∈ b, v p.1 = 0) :
v = 0

Within the span of a triangular basis, its pivot coordinates determine the vector.

source
theorem MIPRE.LowDegree.BinaryLinear.IsPivotBasis.reduce_eq_zero {n t : ℕ} {b : List (Pivot n t)} (hb : IsPivotBasis b) (r : Row n t) (hr : r.1 ∈ pivotSpan b) :
(typedReduce b r).1 = 0

A member of the basis span reduces to zero.

source
theorem MIPRE.LowDegree.BinaryLinear.represents_typedInsert {n t : ℕ} (L : (Fin t → ZMod 2) →ₗ[ZMod 2] Fin n → ZMod 2) (b : List (Pivot n t)) (r : Row n t) (hb : ∀ p ∈ b, Represents L p.2) (hr : Represents L r) (p : Pivot n t) :
p ∈ typedInsert b r → Represents L p.2
source
theorem MIPRE.LowDegree.BinaryLinear.represents_fold_typedInsert {n t : ℕ} (L : (Fin t → ZMod 2) →ₗ[ZMod 2] Fin n → ZMod 2) (rows : List (Row n t)) (b : List (Pivot n t)) (hb : ∀ p ∈ b, Represents L p.2) (hr : ∀ r ∈ rows, Represents L r) (p : Pivot n t) :
p ∈ List.foldl typedInsert b rows → Represents L p.2
source
theorem MIPRE.LowDegree.BinaryLinear.typedBasis_represents {n t : ℕ} (L : (Fin t → ZMod 2) →ₗ[ZMod 2] Fin n → ZMod 2) (rows : List (Row n t)) (hr : ∀ r ∈ rows, Represents L r) (p : Pivot n t) :
p ∈ typedBasis rows → Represents L p.2

Every constructed basis row retains its expression in the original generating family.

source
theorem MIPRE.LowDegree.BinaryLinear.typedReduceStep_error {n t : ℕ} (L : (Fin t → ZMod 2) →ₗ[ZMod 2] Fin n → ZMod 2) (r : Row n t) (p : Pivot n t) (hp : Represents L p.2) :
(typedReduceStep r p).1 + L (typedReduceStep r p).2 = r.1 + L r.2

The vector plus the image of its certificate is unchanged by reduction.

source
theorem MIPRE.LowDegree.BinaryLinear.typedReduce_error {n t : ℕ} (L : (Fin t → ZMod 2) →ₗ[ZMod 2] Fin n → ZMod 2) (b : List (Pivot n t)) (r : Row n t) (hb : ∀ p ∈ b, Represents L p.2) :
(typedReduce b r).1 + L (typedReduce b r).2 = r.1 + L r.2
source
theorem MIPRE.LowDegree.BinaryLinear.solve_certificate {n t : ℕ} (L : (Fin t → ZMod 2) →ₗ[ZMod 2] Fin n → ZMod 2) (b : List (Pivot n t)) (hb : IsPivotBasis b) (hrep : ∀ p ∈ b, Represents L p.2) (v : Fin n → ZMod 2) (hv : v ∈ pivotSpan b) :
L (typedReduce b (v, 0)).2 = v

Reducing a target with an initially zero certificate solves the original system.

source
def MIPRE.LowDegree.BinaryLinear.vectorValue (n : ℕ) (v : Cost.BitStr) :
Fin n → ZMod 2
Equations
Instances For
    source
    @[simp]
    theorem MIPRE.LowDegree.BinaryLinear.vectorValue_vectorBits {n : ℕ} (v : Fin n → ZMod 2) :
    vectorValue n (vectorBits v) = v
    source
    noncomputable def MIPRE.LowDegree.BinaryLinear.solveBitsProg :
    Cost.PolyTimeFun (Cost.Unary × List RawPivot × Cost.BitStr) Cost.BitStr

    Solve using a supplied pivot basis; the certificate width is unary.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.LowDegree.BinaryLinear.solveBitsProg_encoding {n t : ℕ} (b : List (Pivot n t)) (v : Fin n → ZMod 2) :
      solveBitsProg.toFun (Cost.unary t, List.map pivotBits b, vectorBits v) = vectorBits (typedReduce b (v, 0)).2

      Solver output is the canonical fixed-width encoding of its coefficient vector.

      source
      theorem MIPRE.LowDegree.BinaryLinear.solveBitsProg_correct {n t : ℕ} (L : (Fin t → ZMod 2) →ₗ[ZMod 2] Fin n → ZMod 2) (b : List (Pivot n t)) (hb : IsPivotBasis b) (hrep : ∀ p ∈ b, Represents L p.2) (v : Fin n → ZMod 2) (hv : v ∈ pivotSpan b) :
      L (vectorValue t (solveBitsProg.toFun (Cost.unary t, List.map pivotBits b, vectorBits v))) = v

      Correctness of the actual uniform binary solver on every target in the basis span.

      source
      noncomputable def MIPRE.LowDegree.BinaryLinear.basisSolveProg :
      Cost.PolyTimeFun (Cost.Unary × List RawRow × Cost.BitStr) Cost.BitStr

      Construct a basis and solve, all within one ambient polynomial-time program.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.LowDegree.BinaryLinear.basisSolveProg_encoding {n t : ℕ} (rows : List (Row n t)) (v : Fin n → ZMod 2) :
        basisSolveProg.toFun (Cost.unary t, List.map rowBits rows, vectorBits v) = vectorBits (typedReduce (typedBasis rows) (v, 0)).2
        source
        theorem MIPRE.LowDegree.BinaryLinear.basisSolveProg_correct {n t : ℕ} (L : (Fin t → ZMod 2) →ₗ[ZMod 2] Fin n → ZMod 2) (rows : List (Row n t)) (hr : ∀ r ∈ rows, Represents L r) (v : Fin n → ZMod 2) (hv : v ∈ rowSpan rows) :
        L (vectorValue t (basisSolveProg.toFun (Cost.unary t, List.map rowBits rows, vectorBits v))) = v

        The program solves any consistent binary linear system with supplied generator coordinates.