The finite answer decoder for the actual decision kernel

noncomputable def MIPRE.Introspection.DecisionKernel.Answer.pauliDecode {k : ℕ} (E : SAT.BinField k) (m : ℕ) (t : Label) (bs : Cost.BitStr) : QLD.Answer E.carrier m 1

Equations

• MIPRE.Introspection.DecisionKernel.Answer.pauliDecode E m t bs = MIPRE.QLD.PauliAnswerProgram.decodeBits E m 1 (MIPRE.Introspection.DecisionKernel.pauliLabel t) bs

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

The codomain is finite: both the source answer and the Pauli answer have their actual bounded semantic alphabets.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Introspection.DecisionKernel.Answer.decode_pauli {k : ℕ} (E : SAT.BinField k) (m Q R : ℕ) (T : QLD.Ty) (bs : Cost.BitStr) : decode E m Q R (Sum.inl T) bs = ParsedAnswer.pauli (QLD.PauliAnswerProgram.decodeBits E m 1 T bs)

theorem MIPRE.Introspection.DecisionKernel.Answer.questionOfBits_ty (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (T : QLD.Ty) (q : Cost.BitStr) : (QLD.PauliBinaryProgram.questionOfBits k hk hodd j T q).ty = T

theorem MIPRE.Introspection.DecisionKernel.Answer.pauliDecode_format (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (T : QLD.Ty) (q a : Cost.BitStr) : (QLD.PauliBinaryProgram.questionOfBits k hk hodd j T q).fmtOk (pauliDecode (SAT.shoupBinField k hk) (2 ^ j) (Sum.inl T) a) = true

Every decoded Pauli outcome is legal even when its raw input was malformed.

noncomputable def MIPRE.Introspection.DecisionKernel.Answer.pauliProject {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m k : ℕ} (basis : Module.Basis (Fin k) (ZMod 2) F) : QLD.Answer F m 1 → Fin (2 ^ m * k) → CL.𝔽₂

Equations

• MIPRE.Introspection.DecisionKernel.Answer.pauliProject basis (MIPRE.QLD.Answer.pauliAns h) = MIPRE.QLD.PauliFullAnswerProgram.registerVector basis h
• MIPRE.Introspection.DecisionKernel.Answer.pauliProject basis x✝ = 0

noncomputable def MIPRE.Introspection.DecisionKernel.Answer.rawProject (p : PauliSamplerParameters.Parameters) (Q : ℕ) (bs : Cost.BitStr) : Fin Q → CL.𝔽₂

Read the executable projection at a fixed finite register size.

Equations

• MIPRE.Introspection.DecisionKernel.Answer.rawProject p Q bs = MIPRE.CL.ofBits Q (MIPRE.QLD.PauliBinaryProgram.fullAnswer.toFun (p, bs)).2

theorem MIPRE.Introspection.DecisionKernel.Answer.rawProject_pauliDecode (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j m : ℕ) (W : QLD.Bas) (a : Cost.BitStr) (ha : (QLD.PauliAnswerProgram.parser.toFun (QLD.Ty.pauli W, Cost.unary m, Cost.unary k, Cost.unary 1, a)).1 = true) : rawProject (Cost.unary k, Cost.unary j, Cost.unary m) (2 ^ m * k) a = pauliProject (SAT.shoupSelfDualNormalBasis k hk hodd) (pauliDecode (SAT.shoupBinField k hk) m (Sum.inl (QLD.Ty.pauli W)) a)

theorem MIPRE.Introspection.DecisionKernel.program_leftPauli_valid (W : Cost.ClockedUniversalMachine) (V : Verifier 7) (lam n Q R : ℕ) (p : PauliSamplerParameters.Parameters) (T : QLD.Ty) (U : Label) (x y a b : Cost.BitStr) (h : (program W).toFun (canonicalInput V lam n Q R p (Sum.inl T) U x y a b) = true) : QLD.PauliBinaryProgram.endpointValid.toFun (p, T, x, a) = true

theorem MIPRE.Introspection.DecisionKernel.program_rightPauli_valid (W : Cost.ClockedUniversalMachine) (V : Verifier 7) (lam n Q R : ℕ) (p : PauliSamplerParameters.Parameters) (T : Label) (U : QLD.Ty) (x y a b : Cost.BitStr) (h : (program W).toFun (canonicalInput V lam n Q R p T (Sum.inl U) x y a b) = true) : QLD.PauliBinaryProgram.endpointValid.toFun (p, U, y, b) = true