Documentation

MIPRE.Foundations.LowDegree.BinaryComponentsProg

Polynomial-time fixed-space component separation #

source
theorem MIPRE.LowDegree.BinaryLinear.instFactPrimeOfNatNat_mIPRE_3 :
Fact (Nat.Prime 2)
source
noncomputable def MIPRE.LowDegree.BinaryLinear.nonzeroRowProg :
Cost.PolyTimeFun Cost.BitStr Bool
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.LowDegree.BinaryLinear.keepRowProg :
    Cost.PolyTimeFun Cost.BitStr (List Cost.BitStr)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def MIPRE.LowDegree.BinaryLinear.splitBitsProg :
      Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) (List Cost.BitStr)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MIPRE.LowDegree.BinaryLinear.flattenBitsProg :
        Cost.PolyTimeFun (List (List Cost.BitStr)) (List Cost.BitStr)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def MIPRE.LowDegree.BinaryLinear.splitBitsCappedProg :
          Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr × Cost.BitStr) (List Cost.BitStr)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem MIPRE.LowDegree.BinaryLinear.splitBitsCappedProg_apply (u : Cost.Unary) (l : List Cost.BitStr) (b : Cost.BitStr) :
            splitBitsCappedProg.toFun (u, l, b) = splitBitsCapped u l b
            source
            noncomputable def MIPRE.LowDegree.BinaryLinear.componentStep (s : Cost.Unary × List Cost.BitStr) (b : Cost.BitStr) :
            Cost.Unary × List Cost.BitStr
            Equations
            Instances For
              source
              noncomputable def MIPRE.LowDegree.BinaryLinear.componentStepProg :
              Cost.PolyTimeFun ((Cost.Unary × List Cost.BitStr) × Cost.BitStr) (Cost.Unary × List Cost.BitStr)
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem MIPRE.LowDegree.BinaryLinear.splitBitsCapped_width (u : Cost.Unary) (l : List Cost.BitStr) (b : Cost.BitStr) (N : ℕ) (hl : ∀ e ∈ l, List.length e ≤ N) (e : Cost.BitStr) :
                e ∈ splitBitsCapped u l b → List.length e ≤ N
                source
                theorem MIPRE.LowDegree.BinaryLinear.fold_componentStep_width (bs : List Cost.BitStr) (u : Cost.Unary) (l : List Cost.BitStr) (N : ℕ) (hl : ∀ e ∈ l, List.length e ≤ N) (e : Cost.BitStr) :
                e ∈ (List.foldl componentStep (u, l) bs).2 → List.length e ≤ N
                source
                theorem MIPRE.LowDegree.BinaryLinear.fold_componentStep_dimension (bs : List Cost.BitStr) (u : Cost.Unary) (l : List Cost.BitStr) :
                (List.foldl componentStep (u, l) bs).1 = u
                source
                theorem MIPRE.LowDegree.BinaryLinear.fold_componentStep_length (bs : List Cost.BitStr) (u : Cost.Unary) (l : List Cost.BitStr) (N : ℕ) (hu : List.length u ≤ N) (hl : l.length ≤ N) :
                (List.foldl componentStep (u, l) bs).2.length ≤ N
                source
                theorem MIPRE.LowDegree.BinaryLinear.esize_rows_of_width (l : List Cost.BitStr) (N : ℕ) (hl : ∀ e ∈ l, List.length e ≤ N) :
                Cost.esize l ≤ l.length * (4 * N + 2) + 1
                source
                theorem MIPRE.LowDegree.BinaryLinear.componentStep_bounded :
                componentStepProg.FoldBounded (5 * Polynomial.X ^ 2 + 5 * Polynomial.X + 5)
                source
                noncomputable def MIPRE.LowDegree.BinaryLinear.groupComponentsProg :
                Cost.PolyTimeFun Cost.Unary (List Cost.BitStr)

                Split by every computed fixed-space generator. Clipping controls malformed inputs too.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem MIPRE.LowDegree.BinaryLinear.fold_componentStep_encoding {k : ℕ} [NeZero k] (bs l : List (AddMonoidAlgebra (ZMod 2) (Fin k))) (hl : ComponentFamily l) (hb : ∀ b ∈ bs, b * b = b) :
                  List.foldl componentStep (Cost.unary k, List.map (fun (z : AddMonoidAlgebra (ZMod 2) (Fin k)) => vectorBits ((groupCoordinates k) z)) l) (List.map (fun (z : AddMonoidAlgebra (ZMod 2) (Fin k)) => vectorBits ((groupCoordinates k) z)) bs) = (Cost.unary k, List.map (fun (z : AddMonoidAlgebra (ZMod 2) (Fin k)) => vectorBits ((groupCoordinates k) z)) (splitAllComponents l bs))
                  source
                  theorem MIPRE.LowDegree.BinaryLinear.unitBits_group_one (k : ℕ) [NeZero k] :
                  unitBits k 0 = vectorBits ((groupCoordinates k) 1)
                  source
                  theorem MIPRE.LowDegree.BinaryLinear.groupComponentsProg_correct (k : ℕ) [NeZero k] :
                  groupComponentsProg.toFun (Cost.unary k) = List.map (fun (z : AddMonoidAlgebra (ZMod 2) (Fin k)) => vectorBits ((groupCoordinates k) z)) (groupComponents k)

                  The raw program prints precisely the nonzero primitive components, in deterministic order.