Quantitative transport of every dual readout from Hide to Read #
The outcome map is chosen before applying the tested consistency estimate. Consequently the bound is quadratic in the path length and independent of the size of every answer fibre.
Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the strategy is a pair of
POVM families in the two players' algebras, and the same-side distances are the model's
stateSqNorm of the first player's coarse-grained operators.
theorem
MIPRE.Introspection.TypedEstimates.dual_chain_step_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]
[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)
:
∑ z : Option ((ι → F) × (ι → F)),
Ψ.stateSqNorm
((POVMIn.map (reportedDual (L w) m (prefixChainType j i)) (MA (Sum.inr (prefixChainType j i, w), 0))).op z - (POVMIn.map (reportedDual (L w) m (prefixChainType j (i + 1)))
(MA (Sum.inr (prefixChainType j (i + 1), w), 0))).op
z) ≤ 8 * ↑(TypeGraph.edges E X Z ℓ).card * ε
theorem
MIPRE.Introspection.TypedEstimates.hiding_read_dual_chain_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]
[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 ℓ)
:
∑ z : Option ((ι → F) × (ι → F)),
Ψ.stateSqNorm
((POVMIn.map (reportedDual (L w) (↑j) (AuxType.hide j)) (MA (QuestionType.hide w j, 0))).op z - (POVMIn.map (reportedDual (L w) (↑j) AuxType.read) (MA (QuestionType.read w, 0))).op z) ≤ ↑(ℓ - ↑j) ^ 2 * (8 * ↑(TypeGraph.edges E X Z ℓ).card * ε)
Transport one fixed dual readout from its hiding level to Alice's Read.