Documentation

MIPRE.Background.QLD.PauliBinaryPrograms

From raw self-dual Pauli question bits to the actual decision program #

The executable block decoder converts every binary coordinate to its canonical Shoup representation and unpacks the fixed coordinate order. The resulting typed payloads are then passed to the uniform Boolean decision program.

source
noncomputable def MIPRE.QLD.PauliBinaryProgram.coordinateCount :
Cost.PolyTimeFun Introspection.PauliStageProgram.Parameters Cost.Unary
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.QLD.PauliBinaryProgram.coordinateCount_apply (k j m : Cost.Unary) :
    coordinateCount.toFun (k, j, m) = Cost.unary (3 * List.length m + 3)
    source
    noncomputable def MIPRE.QLD.PauliBinaryProgram.fieldsProg :
    Cost.PolyTimeFun (Introspection.PauliStageProgram.Parameters × Cost.BitStr) Introspection.PauliStageProgram.Fields
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.QLD.PauliBinaryProgram.fieldsProg_binaryVector (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j m : ℕ) [NeZero m] (x : PauliCL.Coord m → (SAT.shoupBinField k hk).carrier) :
      fieldsProg.toFun ((Cost.unary k, Cost.unary j, Cost.unary m), CL.toBits ((PauliCL.binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) x)) = PauliCL.fieldEncoding (SAT.shoupBinField k hk) x
      source
      theorem MIPRE.QLD.PauliBinaryProgram.fieldsProg_ofBits (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j m : ℕ) [NeZero m] (bs : Cost.BitStr) (hbs : List.length bs = (3 * m + 3) * k) :
      fieldsProg.toFun ((Cost.unary k, Cost.unary j, Cost.unary m), bs) = PauliCL.fieldEncoding (SAT.shoupBinField k hk) ((PauliCL.binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)).symm (CL.ofBits ((3 * m + 3) * k) bs))

      Every full-length bit string has exactly its inverse-basis field meaning.

      source
      @[reducible, inline]
      abbrev MIPRE.QLD.PauliBinaryProgram.Payload :
      Type
      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev MIPRE.QLD.PauliBinaryProgram.Input :
        Type
        Equations
        Instances For
          source
          noncomputable def MIPRE.QLD.PauliBinaryProgram.endpointProg :
          Cost.PolyTimeFun (Introspection.PauliStageProgram.Parameters × Payload) PauliBooleanProgram.Payload
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def MIPRE.QLD.PauliBinaryProgram.booleanInput :
            Cost.PolyTimeFun Input PauliBooleanProgram.Input
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def MIPRE.QLD.PauliBinaryProgram.program :
              Cost.PolyTimeFun Input Bool
              Equations
              Instances For
                source
                theorem MIPRE.QLD.PauliBinaryProgram.booleanInput_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j m : ℕ) [NeZero m] (T U : Ty) (x y : PauliCL.Coord m → (SAT.shoupBinField k hk).carrier) (a b : Cost.BitStr) :
                booleanInput.toFun ((Cost.unary k, Cost.unary j, Cost.unary m), (T, CL.toBits ((PauliCL.binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) x), a), U, CL.toBits ((PauliCL.binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) y), b) = ((Cost.unary k, Cost.unary j, Cost.unary m), (T, PauliCL.fieldEncoding (SAT.shoupBinField k hk) x, a), U, PauliCL.fieldEncoding (SAT.shoupBinField k hk) y, b)