Kernel soundness in the finite semantic answer alphabet #
noncomputable def
MIPRE.Introspection.DecisionKernel.finiteSourcePredicate
{n Q R : ℕ}
(V : Verifier 7)
(hs : V.sampler.dim (2 ^ n) ≤ Q)
(x y : Fin Q → CL.𝔽₂)
(a b : Verifier.Answers R)
:
Equations
- MIPRE.Introspection.DecisionKernel.finiteSourcePredicate V hs x y a b = MIPRE.Introspection.AuxiliaryDecision.sourcePredicate V hs x y ↑a ↑b
Instances For
noncomputable def
MIPRE.Introspection.DecisionKernel.finitePauliCheck
(k : ℕ)
(hk : 1 ≤ k)
[NeZero k]
(hodd : Odd k)
(j : ℕ)
(hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier)
(x y : Cost.BitStr)
(T U : QLD.Ty)
:
QLD.Answer (SAT.shoupBinField k hk).carrier (2 ^ j) 1 → QLD.Answer (SAT.shoupBinField k hk).carrier (2 ^ j) 1 → Bool
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPRE.Introspection.DecisionKernel.program_sound
(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 a b : Cost.BitStr)
(h :
(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 a
b) = true)
:
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
(Answer.decode (SAT.shoupBinField k hk) (2 ^ j) (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) T a)
(Answer.decode (SAT.shoupBinField k hk) (2 ^ j) (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) U b) = true
Accepted raw tuples decode into the actual finite quotient game. Neither the Pauli field answers nor the original source answers retain an infinite byte alphabet.