Honest completeness of the actual decision kernel #
theorem
MIPRE.Introspection.DecisionKernel.mapAnswer_pauli
{V : Type u_1}
{A : Type u_2}
{B : Type u_3}
{PA : Type u_4}
(f : A → B)
(a : ParsedAnswer V A PA)
(c : PA)
:
theorem
MIPRE.Introspection.DecisionKernel.toRaw_pauli_inv
{k m Q R : ℕ}
(E : SAT.BinField k)
(a : ParsedAnswer (Fin Q → CL.𝔽₂) (Verifier.Answers R) (QLD.Answer E.carrier m 1))
(c : Cost.BitStr)
(h : Answer.toRaw E a = ParsedAnswer.pauli c)
:
∃ (d : QLD.Answer E.carrier m 1), a = ParsedAnswer.pauli d ∧ c = QLD.PauliAnswerProgram.answerBits E d
theorem
MIPRE.Introspection.DecisionKernel.encoded_quotient
{lam n : ℕ}
(V : Verifier 7)
(k : ℕ)
(hk : 1 ≤ k)
[NeZero k]
(hodd : Odd k)
(j : ℕ)
(hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier)
(hs : V.sampler.dim (2 ^ n) ≤ 2 ^ 2 ^ j * k)
(T U : Label)
(x y : Cost.BitStr)
(a b :
ParsedAnswer (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂) (Verifier.Answers ((2 ^ n) ^ lam))
(QLD.Answer (SAT.shoupBinField k hk).carrier (2 ^ j) 1))
(ha : Answer.PauliFormatted k hk hodd j (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) T x a)
(hb : Answer.PauliFormatted k hk hodd j (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) U y b)
(h :
AuxiliaryQuotient.check (AuxiliaryDecision.padded V hs) (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z)
(Answer.pauliProject (SAT.shoupSelfDualNormalBasis k hk hodd)) (finiteSourcePredicate V hs)
(finitePauliCheck k hk hodd j hm x y) T U a b = true)
:
AuxiliaryQuotient.check (AuxiliaryDecision.padded V hs) (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z)
(Answer.rawProject (Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)) (2 ^ 2 ^ j * k))
(AuxiliaryDecision.sourcePredicate V hs) (rawPauliCheck k hk hodd j hm x y) T U
(Answer.toRaw (SAT.shoupBinField k hk) a) (Answer.toRaw (SAT.shoupBinField k hk) b) = true
Encoding bounded source answers and legal Pauli answers preserves every accepted semantic quotient comparison.
theorem
MIPRE.Introspection.DecisionKernel.guarded_pauli
(W : Cost.ClockedUniversalMachine)
(ctx : AuxiliarySource.Context)
(bounds : AuxiliaryDecision.Bounds)
(t u : QLD.Ty)
(a b : Cost.BitStr)
(h : t = u → a = b)
:
theorem
MIPRE.Introspection.DecisionKernel.auxiliary_encoded_complete
(W : Cost.ClockedUniversalMachine)
{lam n : ℕ}
(V : Verifier 7)
(hV : V.IsBounded lam)
(hn : 1 ≤ n)
(k : ℕ)
(hk : 1 ≤ k)
[NeZero k]
(hodd : Odd k)
(j : ℕ)
(hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier)
(hs : V.sampler.dim (2 ^ n) ≤ 2 ^ 2 ^ j * k)
(hQ : 4 ≤ 2 ^ 2 ^ j * k)
(hR : 3 * (2 ^ n) ^ lam ≤ 2 ^ 2 ^ j * k)
(T U : Label)
(x y : Cost.BitStr)
(a b :
ParsedAnswer (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂) (Verifier.Answers ((2 ^ n) ^ lam))
(QLD.Answer (SAT.shoupBinField k hk).carrier (2 ^ j) 1))
(ha : Answer.PauliFormatted k hk hodd j (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) T x a)
(hb : Answer.PauliFormatted k hk hodd j (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) U y b)
(hga : PrefixGuard.holds (AuxiliaryDecision.padded V hs) T a)
(hgb : PrefixGuard.holds (AuxiliaryDecision.padded V hs) U b)
(hsa : AuxiliaryDecision.sourceOutput (V.sampler.dim (2 ^ n)) T (Answer.toRaw (SAT.shoupBinField k hk) a))
(hsb : AuxiliaryDecision.sourceOutput (V.sampler.dim (2 ^ n)) U (Answer.toRaw (SAT.shoupBinField k hk) b))
(h :
AuxiliaryQuotient.check (AuxiliaryDecision.padded V hs) (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z)
(Answer.pauliProject (SAT.shoupSelfDualNormalBasis k hk hodd)) (finiteSourcePredicate V hs)
(finitePauliCheck k hk hodd j hm x y) T U a b = true)
:
(auxiliary W).toFun
(canonicalInput V lam n (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) (Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)) T U x y
(Answer.bits (SAT.shoupBinField k hk) a) (Answer.bits (SAT.shoupBinField k hk) b)) = true
The auxiliary part needs a full zero prefix only when one endpoint has an auxiliary answer; Pauli-only pairs reduce to their byte consistency check.
theorem
MIPRE.Introspection.DecisionKernel.program_complete
(W : Cost.ClockedUniversalMachine)
{lam n : ℕ}
(V : Verifier 7)
(hV : V.IsBounded lam)
(hn : 1 ≤ n)
(k : ℕ)
(hk : 1 ≤ k)
[NeZero k]
(hodd : Odd k)
(j : ℕ)
(hj : j ≤ k)
(hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier)
(hs : V.sampler.dim (2 ^ n) ≤ 2 ^ 2 ^ j * k)
(hQ : 4 ≤ 2 ^ 2 ^ j * k)
(hR : 3 * (2 ^ n) ^ lam ≤ 2 ^ 2 ^ j * k)
(T U : Label)
(x y : Cost.BitStr)
(hx : List.length x = (3 * 2 ^ j + 3) * k)
(hy : List.length y = (3 * 2 ^ j + 3) * k)
(a b :
ParsedAnswer (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂) (Verifier.Answers ((2 ^ n) ^ lam))
(QLD.Answer (SAT.shoupBinField k hk).carrier (2 ^ j) 1))
(ha : Answer.PauliFormatted k hk hodd j (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) T x a)
(hb : Answer.PauliFormatted k hk hodd j (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) U y b)
(hga : PrefixGuard.holds (AuxiliaryDecision.padded V hs) T a)
(hgb : PrefixGuard.holds (AuxiliaryDecision.padded V hs) U b)
(hsa : AuxiliaryDecision.sourceOutput (V.sampler.dim (2 ^ n)) T (Answer.toRaw (SAT.shoupBinField k hk) a))
(hsb : AuxiliaryDecision.sourceOutput (V.sampler.dim (2 ^ n)) U (Answer.toRaw (SAT.shoupBinField k hk) b))
(h :
AuxiliaryQuotient.check (AuxiliaryDecision.padded V hs) (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z)
(Answer.pauliProject (SAT.shoupSelfDualNormalBasis k hk hodd)) (finiteSourcePredicate V hs)
(finitePauliCheck k hk hodd j hm x y) T U a b = true)
:
(program W).toFun
(canonicalInput V lam n (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) (Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)) T U x y
(Answer.bits (SAT.shoupBinField k hk) a) (Answer.bits (SAT.shoupBinField k hk) b)) = true
The complete executable kernel accepts the honest finite encodings. All hypotheses concern the semantic game or the honest outcome support.
theorem
MIPRE.Introspection.DecisionKernel.program_complete_numbered
(W : Cost.ClockedUniversalMachine)
{lam n : ℕ}
(V : Verifier 7)
(hV : V.IsBounded lam)
(hn : 1 ≤ n)
(k : ℕ)
(hk : 1 ≤ k)
[NeZero k]
(hodd : Odd k)
(j : ℕ)
(hj : j ≤ k)
(hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier)
(hs : V.sampler.dim (2 ^ n) ≤ 2 ^ 2 ^ j * k)
(hQ : 4 ≤ 2 ^ 2 ^ j * k)
(hR : 3 * (2 ^ n) ^ lam ≤ 2 ^ 2 ^ j * k)
(χ : (SAT.shoupBinField k hk).carrier → Fin (2 ^ j))
(T U : Label)
(x y : Fin ((3 * 2 ^ j + 3) * k) → CL.𝔽₂)
(a b :
ParsedAnswer (Fin (2 ^ 2 ^ j * k) → CL.𝔽₂) (Verifier.Answers ((2 ^ n) ^ lam))
(QLD.Answer (SAT.shoupBinField k hk).carrier (2 ^ j) 1))
(ha : Answer.PauliFormatted k hk hodd j (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) T (CL.toBits x) a)
(hb : Answer.PauliFormatted k hk hodd j (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) U (CL.toBits y) b)
(hga : PrefixGuard.holds (AuxiliaryDecision.padded V hs) T a)
(hgb : PrefixGuard.holds (AuxiliaryDecision.padded V hs) U b)
(hsa : AuxiliaryDecision.sourceOutput (V.sampler.dim (2 ^ n)) T (Answer.toRaw (SAT.shoupBinField k hk) a))
(hsb : AuxiliaryDecision.sourceOutput (V.sampler.dim (2 ^ n)) U (Answer.toRaw (SAT.shoupBinField k hk) b))
(h :
(NumberedComplete.game (QLD.PauliFullAnswerProgram.registerNumbering (2 ^ j) k).symm (AuxiliaryDecision.padded V hs)
(finiteSourcePredicate V hs) hm (SAT.shoupSelfDualNormalBasis k hk hodd) χ
(QLD.PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk))).D
(T, x) (U, y) a b = true)
:
(program W).toFun
(canonicalInput V lam n (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) (Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)) T U
(CL.toBits x) (CL.toBits y) (Answer.bits (SAT.shoupBinField k hk) a) (Answer.bits (SAT.shoupBinField k hk) b)) = true
The accepted finite pair can be supplied directly from the numbered quotient game used by the honest strategy construction.