Documentation

MIPRE.Foundations.LowDegree.BinaryBasisProg

Uniform construction of a binary pivot basis #

source
def MIPRE.LowDegree.BinaryLinear.firstOne (v : Cost.BitStr) :
ℕ

First set bit, or the list length if the vector is zero.

Equations
Instances For
    source
    theorem MIPRE.LowDegree.BinaryLinear.firstOne_le (v : Cost.BitStr) :
    firstOne v ≤ List.length v
    source
    theorem MIPRE.LowDegree.BinaryLinear.firstOne_getD (v : Cost.BitStr) (h : firstOne v < List.length v) :
    List.getD v (firstOne v) false = true
    source
    theorem MIPRE.LowDegree.BinaryLinear.firstOne_getD_iff (v : Cost.BitStr) :
    List.getD v (firstOne v) false = true ↔ firstOne v < List.length v
    source
    noncomputable def MIPRE.LowDegree.BinaryLinear.firstOneStep :
    Cost.PolyTimeFun (ℕ × Bool) ℕ
    Equations
    Instances For
      source
      theorem MIPRE.LowDegree.BinaryLinear.firstOne_fold (v : Cost.BitStr) :
      List.foldl firstOneStep.step 0 (List.reverse v) = firstOne v
      source
      noncomputable def MIPRE.LowDegree.BinaryLinear.firstOneProg :
      Cost.PolyTimeFun Cost.BitStr ℕ

      Finding a pivot scans the vector, without enumerating its binary magnitude.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem MIPRE.LowDegree.BinaryLinear.firstOneProg_apply (v : Cost.BitStr) :
        firstOneProg.toFun v = firstOne v
        source
        def MIPRE.LowDegree.BinaryLinear.insertRow (b : List RawPivot) (r : RawRow) :
        List RawPivot

        Reduce the candidate, then append it only when its remainder has a pivot.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def MIPRE.LowDegree.BinaryLinear.insertRowProg :
          Cost.PolyTimeFun (List RawPivot × RawRow) (List RawPivot)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem MIPRE.LowDegree.BinaryLinear.insertRowProg_apply (b : List RawPivot) (r : RawRow) :
            insertRowProg.toFun (b, r) = insertRow b r
            source
            theorem MIPRE.LowDegree.BinaryLinear.insertRow_size (b : List RawPivot) (r : RawRow) :
            Cost.esize (insertRow b r) ≤ Cost.esize b + 20 * Cost.esize r + 20

            The new row's encoded size is bounded by the input row, independent of the existing basis. This additive bound is the polynomial fold invariant.

            source
            def MIPRE.LowDegree.BinaryLinear.basisRows (rows : List RawRow) :
            List RawPivot

            The complete forward elimination scan.

            Equations
            Instances For
              source
              noncomputable def MIPRE.LowDegree.BinaryLinear.basisRowsProg :
              Cost.PolyTimeFun (List RawRow) (List RawPivot)

              Uniform polynomial-time construction of a pivot basis with coefficient certificates.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem MIPRE.LowDegree.BinaryLinear.basisRowsProg_apply (rows : List RawRow) :
                basisRowsProg.toFun rows = basisRows rows