Documentation

MIPRE.Foundations.LowDegree.BinaryElimination

Binary elimination with coefficient certificates #

Each row carries both its vector and a coefficient vector describing that vector in the original generating family. Reduction XORs both components together. The program is uniformly polynomial-time even for malformed pivots and rows.

source
@[reducible, inline]
abbrev MIPRE.LowDegree.BinaryLinear.RawRow :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev MIPRE.LowDegree.BinaryLinear.RawPivot :
    Type
    Equations
    Instances For
      source
      def MIPRE.LowDegree.BinaryLinear.reduceStep (r : RawRow) (b : RawPivot) :
      RawRow
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def MIPRE.LowDegree.BinaryLinear.reduceRows (b : List RawPivot) (r : RawRow) :
        RawRow
        Equations
        Instances For
          source
          theorem MIPRE.LowDegree.BinaryLinear.reduceStep_width (r : RawRow) (b : RawPivot) :
          List.length (reduceStep r b).1 ≤ List.length r.1 ∧ List.length (reduceStep r b).2 ≤ List.length r.2
          source
          theorem MIPRE.LowDegree.BinaryLinear.reduceRows_width (b : List RawPivot) (r : RawRow) :
          List.length (reduceRows b r).1 ≤ List.length r.1 ∧ List.length (reduceRows b r).2 ≤ List.length r.2
          source
          @[reducible, inline]
          abbrev MIPRE.LowDegree.BinaryLinear.Row (n t : ℕ) :
          Type
          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev MIPRE.LowDegree.BinaryLinear.Pivot (n t : ℕ) :
            Type
            Equations
            Instances For
              source
              def MIPRE.LowDegree.BinaryLinear.rowBits {n t : ℕ} (r : Row n t) :
              RawRow
              Equations
              Instances For
                source
                def MIPRE.LowDegree.BinaryLinear.pivotBits {n t : ℕ} (p : Pivot n t) :
                RawPivot
                Equations
                Instances For
                  source
                  def MIPRE.LowDegree.BinaryLinear.typedReduceStep {n t : ℕ} (r : Row n t) (p : Pivot n t) :
                  Row n t
                  Equations
                  Instances For
                    source
                    def MIPRE.LowDegree.BinaryLinear.typedReduce {n t : ℕ} (b : List (Pivot n t)) (r : Row n t) :
                    Row n t
                    Equations
                    Instances For
                      source
                      theorem MIPRE.LowDegree.BinaryLinear.getD_vectorBits {n : ℕ} (v : Fin n → ZMod 2) (j : Fin n) :
                      List.getD (vectorBits v) (↑j) false = bit (v j)
                      source
                      theorem MIPRE.LowDegree.BinaryLinear.reduceStep_rowBits {n t : ℕ} (r : Row n t) (p : Pivot n t) :
                      reduceStep (rowBits r) (pivotBits p) = rowBits (typedReduceStep r p)

                      A raw XOR step is the corresponding operation on both typed vectors.

                      source
                      theorem MIPRE.LowDegree.BinaryLinear.reduceRows_rowBits {n t : ℕ} (b : List (Pivot n t)) (r : Row n t) :
                      reduceRows (List.map pivotBits b) (rowBits r) = rowBits (typedReduce b r)

                      The entire executable reduction agrees with typed binary elimination.

                      source
                      def MIPRE.LowDegree.BinaryLinear.Represents {n t : ℕ} (L : (Fin t → ZMod 2) →ₗ[ZMod 2] Fin n → ZMod 2) (r : Row n t) :
                      Prop

                      A row carries a valid expression in a fixed original generating family.

                      Equations
                      Instances For
                        source
                        theorem MIPRE.LowDegree.BinaryLinear.represents_typedReduceStep {n t : ℕ} (L : (Fin t → ZMod 2) →ₗ[ZMod 2] Fin n → ZMod 2) (r : Row n t) (p : Pivot n t) (hr : Represents L r) (hp : Represents L p.2) :
                        Represents L (typedReduceStep r p)
                        source
                        theorem MIPRE.LowDegree.BinaryLinear.represents_typedReduce {n t : ℕ} (L : (Fin t → ZMod 2) →ₗ[ZMod 2] Fin n → ZMod 2) (b : List (Pivot n t)) (r : Row n t) (hr : Represents L r) (hb : ∀ p ∈ b, Represents L p.2) :
                        Represents L (typedReduce b r)

                        Reduction preserves the coefficient certificate in the original family.

                        source
                        noncomputable def MIPRE.LowDegree.BinaryLinear.reduceStepProg :
                        Cost.PolyTimeFun (RawRow × RawPivot) RawRow
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem MIPRE.LowDegree.BinaryLinear.reduceStep_bounded :
                          reduceStepProg.FoldBounded (5 * Polynomial.X + 5)
                          source
                          noncomputable def MIPRE.LowDegree.BinaryLinear.reduceRowsProg :
                          Cost.PolyTimeFun (List RawPivot × RawRow) RawRow

                          Uniform, certificate-preserving binary elimination along a supplied pivot list.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[simp]
                            theorem MIPRE.LowDegree.BinaryLinear.reduceRowsProg_apply (b : List RawPivot) (r : RawRow) :
                            reduceRowsProg.toFun (b, r) = reduceRows b r