Documentation

MIPRE.Background.QLD.PauliFullAnswerPrograms

Executable full Pauli answers in the self-dual register coordinates #

Full field tables are enumerated by the same little-endian cube enumeration as the Pauli evaluator. Each entry is then expanded in the proved self-dual basis. This fixes the full-register numbering explicitly.

source
noncomputable def MIPRE.QLD.PauliFullAnswerProgram.registerNumbering (m k : ℕ) :
(Fin m → Bool) × Fin k ≃ Fin (2 ^ m * k)
Equations
Instances For
    source
    noncomputable def MIPRE.QLD.PauliFullAnswerProgram.registerVector {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m k : ℕ} (b : Module.Basis (Fin k) (ZMod 2) F) (h : (Fin m → Bool) → F) :
    Fin (2 ^ m * k) → ZMod 2
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.QLD.PauliFullAnswerProgram.registerVector_apply {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m k : ℕ} (b : Module.Basis (Fin k) (ZMod 2) F) (h : (Fin m → Bool) → F) (i : Fin (2 ^ m)) (j : Fin k) :
      registerVector b h (finProdFinEquiv (i, j)) = b.equivFun (h ((Introspection.FieldTableProgram.cubeEnumeration m).symm i)) j
      source
      theorem MIPRE.QLD.PauliFullAnswerProgram.registerVector_bits {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m k : ℕ} (b : Module.Basis (Fin k) (ZMod 2) F) (h : (Fin m → Bool) → F) :
      CL.toBits (registerVector b h) = (List.ofFn fun (i : Fin (2 ^ m)) => LowDegree.BinaryLinear.vectorBits (b.equivFun (h ((Introspection.FieldTableProgram.cubeEnumeration m).symm i)))).flatten
      source
      @[reducible, inline]
      abbrev MIPRE.QLD.PauliFullAnswerProgram.Input :
      Type
      Equations
      Instances For
        source
        noncomputable def MIPRE.QLD.PauliFullAnswerProgram.program :
        Cost.PolyTimeFun Input (Bool × Cost.BitStr)

        The validity flag and the full-register bits, in one polynomial-time program.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MIPRE.QLD.PauliFullAnswerProgram.program_answerBits (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (m d : ℕ) (h : (Fin m → Bool) → (SAT.shoupBinField k hk).carrier) :
          program.toFun (Cost.unary m, Cost.unary k, PauliAnswerProgram.answerBits (SAT.shoupBinField k hk) (Answer.pauliAns h)) = (true, CL.toBits (registerVector (SAT.shoupSelfDualNormalBasis k hk hodd) h))