Documentation

MIPRE.Background.Introspection.DecisionKernelEncoding

Encoding finite honest answers for the actual decision kernel #

source
noncomputable def MIPRE.Introspection.DecisionKernel.Answer.toRaw {k m Q R : ℕ} (E : SAT.BinField k) (a : ParsedAnswer (Fin Q → CL.𝔽₂) (Verifier.Answers R) (QLD.Answer E.carrier m 1)) :
ParsedAnswer (Fin Q → CL.𝔽₂) Cost.BitStr Cost.BitStr

Forget only the finite source-answer bound and encode the Pauli payload. All three full-register auxiliary formats retain their exact coordinates.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.Introspection.DecisionKernel.Answer.bits {k m Q R : ℕ} (E : SAT.BinField k) (a : ParsedAnswer (Fin Q → CL.𝔽₂) (Verifier.Answers R) (QLD.Answer E.carrier m 1)) :
    Cost.BitStr
    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.Introspection.DecisionKernel.Answer.toRaw_pauli {k m Q R : ℕ} (E : SAT.BinField k) (a : QLD.Answer E.carrier m 1) :
      toRaw E (ParsedAnswer.pauli a) = ParsedAnswer.pauli (QLD.PauliAnswerProgram.answerBits E a)
      source
      theorem MIPRE.Introspection.DecisionKernel.Answer.toRaw_eq_map {k m Q R : ℕ} (E : SAT.BinField k) (T : Label) (a : ParsedAnswer (Fin Q → CL.𝔽₂) (Verifier.Answers R) (QLD.Answer E.carrier m 1)) :
      toRaw E a = ParsedAnswer.mapPauli (fun (x : QuestionType QLD.Ty 7) => QLD.PauliAnswerProgram.answerBits E) T (ParsedAnswer.mapAnswer Subtype.val a)
      source
      def MIPRE.Introspection.DecisionKernel.Answer.PauliFormatted (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j Q R : ℕ) (T : Label) (x : Cost.BitStr) (a : ParsedAnswer (Fin Q → CL.𝔽₂) (Verifier.Answers R) (QLD.Answer (SAT.shoupBinField k hk).carrier (2 ^ j) 1)) :
      Prop

      Pauli format is the actual question's finite answer constructor condition.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.Introspection.DecisionKernel.Answer.parser_answerBits {k m : ℕ} (E : SAT.BinField k) (hk : 1 ≤ k) (q : QLD.Question E.carrier m) (a : QLD.Answer E.carrier m 1) (ha : q.fmtOk a = true) :
        (QLD.PauliAnswerProgram.parser.toFun (q.ty, Cost.unary m, Cost.unary k, Cost.unary 1, QLD.PauliAnswerProgram.answerBits E a)).1 = true
        source
        theorem MIPRE.Introspection.DecisionKernel.Answer.rawProject_answerBits (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j m : ℕ) (W : QLD.Bas) (q : QLD.Question (SAT.shoupBinField k hk).carrier m) (a : QLD.Answer (SAT.shoupBinField k hk).carrier m 1) (hq : q.ty = QLD.Ty.pauli W) (ha : q.fmtOk a = true) :
        rawProject (Cost.unary k, Cost.unary j, Cost.unary m) (2 ^ m * k) (QLD.PauliAnswerProgram.answerBits (SAT.shoupBinField k hk) a) = pauliProject (SAT.shoupSelfDualNormalBasis k hk hodd) a
        source
        @[simp]
        theorem MIPRE.Introspection.DecisionKernel.Answer.fits_toRaw {k m Q R : ℕ} (E : SAT.BinField k) (T : Label) (a : ParsedAnswer (Fin Q → CL.𝔽₂) (Verifier.Answers R) (QLD.Answer E.carrier m 1)) :
        TypedPredicate.fits T (toRaw E a) = TypedPredicate.fits T a
        source
        theorem MIPRE.Introspection.DecisionKernel.Answer.answerBound_toRaw {k m Q R : ℕ} (E : SAT.BinField k) (a : ParsedAnswer (Fin Q → CL.𝔽₂) (Verifier.Answers R) (QLD.Answer E.carrier m 1)) :
        AuxiliaryDecision.answerBound R (toRaw E a)
        source
        theorem MIPRE.Introspection.DecisionKernel.Answer.prefixGuard_toRaw {k m Q R : ℕ} (E : SAT.BinField k) (L : Bool → CL.CLFun CL.𝔽₂ (Fin Q) 7) (T : Label) (a : ParsedAnswer (Fin Q → CL.𝔽₂) (Verifier.Answers R) (QLD.Answer E.carrier m 1)) :
        PrefixGuard.holds L T (toRaw E a) ↔ PrefixGuard.holds L T a
        source
        theorem MIPRE.Introspection.DecisionKernel.Answer.flatten_vecBits_length {k m : ℕ} (E : SAT.BinField k) (v : Fin m → E.carrier) :
        (E.vecBits v).flatten.length = m * k
        source
        theorem MIPRE.Introspection.DecisionKernel.Answer.pauliBits_length_le {k m : ℕ} (E : SAT.BinField k) (hm : 1 ≤ m) (hQ : 3 ≤ 2 ^ m * k) (a : QLD.Answer E.carrier m 1) :
        List.length (QLD.PauliAnswerProgram.answerBits E a) ≤ 2 ^ m * k

        All semantic Pauli constructors have short encodings at degree one, including constructors excluded by the eventual question format.

        source
        theorem MIPRE.Introspection.DecisionKernel.Answer.bits_length_le_cutoff {k m R : ℕ} (E : SAT.BinField k) (hm : 1 ≤ m) (hQ : 4 ≤ 2 ^ m * k) (hR : 3 * R ≤ 2 ^ m * k) (a : ParsedAnswer (Fin (2 ^ m * k) → CL.𝔽₂) (Verifier.Answers R) (QLD.Answer E.carrier m 1)) :
        List.length (bits E a) ≤ DecisionCompiler.answerBound (2 ^ m * k) R

        Every finite honest answer lies below the actual compiler's outer cutoff.