Transferring honest hiding rigidity through the actual consistency loop

The two ideal families are exact mirrors on the EPR register with arbitrary auxiliaries. The parsed game's same-type test therefore transfers Bob's estimate to Alice with error 4 |E| epsilon + 2 beta. No symmetry of the Pauli predicate or of the full game is required.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the EPR register with arbitrary auxiliaries is the register model Ξ.reg (ι → F), exact mirrors are vector identities, and the honest families enter as smulKron 1 _.

theorem MIPRE.Introspection.sum_xSqNorm_mirror_transfer {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} [Fintype I] (M P : I → 𝒜) (N Q : I → ℬ) (hmirror : ∀ (i : I), (Ψ.π (Ψ.πA (P i))) Ψ.ψ = (Ψ.π (Ψ.πB (Q i))) Ψ.ψ) : ∑ i : I, Ψ.xSqNorm (M i) (Q i) ≤ 2 * ∑ i : I, Ψ.xSqNorm (M i) (N i) + 2 * ∑ i : I, Ψ.xSqNorm (P i) (N i)

An exact ideal mirror and one actual consistency relation transfer rigidity to the other party without changing the outcome alphabet.

noncomputable def MIPRE.Introspection.TypedEstimates.hidingAliceError {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_7} {𝒜 : Type u_8} {ℬ : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (L : Bool → CL.CLFun F ι ℓ) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜)) (j : Fin ℓ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Introspection.TypedEstimates.hidingBobError {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_7} {𝒜 : Type u_8} {ℬ : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (L : Bool → CL.CLFun F ι ℓ) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ)) (j : Fin ℓ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.TypedEstimates.hidingBobError_nonneg {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 ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (L : Bool → CL.CLFun F ι ℓ) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ)) (j : Fin ℓ) : 0 ≤ hidingBobError L w hL Ξ MB j

theorem MIPRE.Introspection.TypedEstimates.hiding_register_orientation {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 ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (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) (Matrix (ι → F) (ι → F) 𝒜)) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ)) {ε : ℝ} (hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (j : Fin ℓ) : hidingAliceError L w hL Ξ MA j ≤ 4 * ↑(TypeGraph.edges E X Z ℓ).card * ε + 2 * hidingBobError L w hL Ξ MB j

The same-type parsed test supplies the orientation transfer. The actual measurements may be arbitrary POVMs in this lemma.