The actual Pauli-X/first-hiding test #
Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the agreement estimate takes
a model Ψ with ‖Ψ.ψ‖ = 1 and measurements POVMIn _ 𝒜, POVMIn _ ℬ, and is the model
instance of pauli_aux_agreement_estimate. The two acceptance statements concern answers only
and are unchanged.
theorem
MIPRE.Introspection.TypedEstimates.hidingCoarse_zero_hide
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{A : Type u_6}
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
{ℓ : ℕ}
(P : CL.CLFun F ι ℓ)
(y yp x : ι → F)
:
hidingCoarse P 0 (ParsedAnswer.hide y yp x) = some (0, (CL.proj (P.factorOfPrefix 0 0)) yp, (CL.proj (P.factorOfPrefix 0 0)ᶜ) x)
theorem
MIPRE.Introspection.TypedEstimates.hiding_first_accepts
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{A : Type u_6}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(X Z : PauliType)
(projectPauli : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool)
(w : Bool)
(k : Fin ℓ)
(hk : ↑k = 0)
(a b : ParsedAnswer (ι → F) A PauliAnswer)
(hab : TypedPredicate.check L X Z projectPauli D DP (Sum.inl X) (Sum.inr (AuxType.hide k, w)) a b = true)
:
This implication is over the complete parsed alphabet; acceptance excludes every malformed constructor before the Pauli-X comparison is used.
theorem
MIPRE.Introspection.TypedEstimates.hiding_first_agreement_estimate
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(projectPauli : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
(Ψ : BipartiteModel 𝒞 𝒜 ℬ)
(hΨ : ‖Ψ.ψ‖ = 1)
(MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) 𝒜)
(MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) ℬ)
{ε : ℝ}
(hfail : 1 - Ψ.povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε)
(w : Bool)
(k : Fin ℓ)
(hk : ↑k = 0)
(qX : κ → ZMod 2)
(hqX : ∀ (z : κ → ZMod 2), (P X).eval z = qX)
:
∑ z : Option ((ι → F) × (ι → F) × (ι → F)),
Ψ.xSqNorm
((POVMIn.map
(fun (a : ParsedAnswer (ι → F) A PauliAnswer) =>
Option.map (Honest.firstHideAnswer (L w)) (pauliProjection projectPauli a))
(MA (Sum.inl X, qX))).op
z)
((POVMIn.map (hidingCoarse (L w) 0) (MB (QuestionType.hide w k, 0))).op z) ≤ 2 * ↑(TypeGraph.edges E X Z ℓ).card * ε
Actual game failure controls the first hiding coarse family against the tested coarse Pauli-X family, on either player's full local carrier.