Bob's reported-prefix chain #
The same actual oriented tests suffice for the right-party estimate: the loop at each earlier endpoint supplies the common Alice measurement. No symmetry of the supplied Pauli decision predicate is required.
Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the right-party estimates are
the left-party ones in the exchanged model Ψ.swap.
theorem
MIPRE.Introspection.TypedEstimates.prefix_chain_step_estimate_bob
{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]
[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)
(hL : (L w).SupportedOn Finset.univ)
(j : Fin ℓ)
(m : ℕ)
(hm : m ≤ ↑j)
(i : ℕ)
(hi : i < ℓ - ↑j + 1)
:
∑ z : Option (ι → F),
Ψ.swap.stateSqNorm
((POVMIn.map (reportedPrefix (L w) m (prefixChainType j i)) (MB (Sum.inr (prefixChainType j i, w), 0))).op z - (POVMIn.map (reportedPrefix (L w) m (prefixChainType j (i + 1)))
(MB (Sum.inr (prefixChainType j (i + 1), w), 0))).op
z) ≤ 8 * ↑(TypeGraph.edges E X Z ℓ).card * ε
The actual next edge and the earlier loop compare Bob's two prefix
measurements with the same 8 |E| ε loss.
theorem
MIPRE.Introspection.TypedEstimates.hiding_introspect_prefix_estimate_bob
{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]
[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)
(hL : (L w).SupportedOn Finset.univ)
(j : Fin ℓ)
(m : ℕ)
(hm : m ≤ ↑j)
:
∑ z : Option (ι → F),
Ψ.snorm
(Ψ.πB
((POVMIn.map (reportedPrefix (L w) m (AuxType.hide j)) (MB (QuestionType.hide w j, 0))).op z - (POVMIn.map (reportedPrefix (L w) m AuxType.introspect) (MB (QuestionType.introspect w, 0))).op z)) ^ 2 ≤ ↑(ℓ - ↑j + 1) ^ 2 * (8 * ↑(TypeGraph.edges E X Z ℓ).card * ε)
Bob's version of the actual prefix chain, in the right-party state norm used by conditional normalizer replacement.