Read rigidity from the full hiding family

First discard the unused X tail across the two players, using projective consistency. Then transport the resulting fixed dual readout along the actual hiding-to-Read chain. No same-party coarse-distance contraction is used.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the EPR seed beside an arbitrary auxiliary state is the register model Ξ.reg (ι → F) of a normalized model Ξ, the strategy is a pair of POVM families of matrices over ι → F with entries in Ξ's algebras, and the honest dual readout readDualOp, a complex register matrix, acts as smulKron 1 _ for either player. Its exact mirror is the vector identity π (πA _) ψ = π (πB _) ψ, coarse-grained from the mirror of the hiding family by fibSum_mirror; coarse-graining a POVM of the model is POVMIn.map, and of an embedded register family fibSumIn_smulKron_one.

noncomputable def MIPRE.Introspection.Honest.readDualOp {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) (b : Option ((ι → F) × (ι → F))) : Matrix (ι → F) (ι → F) ℂ

The ideal joint prefix/dual measurement, with the unused X tail summed out.

Equations

• MIPRE.Introspection.Honest.readDualOp P k h = MIPRE.fibSum (MIPRE.Introspection.Honest.hideCoarseOp P k h) MIPRE.Introspection.TypedEstimates.hidingForgetTail

theorem MIPRE.Introspection.Honest.readDualOp_isPVM {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) : IsPVM (readDualOp P k h)

theorem MIPRE.Introspection.Honest.readDualOp_registerState_mirror {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (i : Option ((ι → F) × (ι → F))) : ((Ξ.reg (ι → F)).π ((Ξ.reg (ι → F)).πA (smulKron 1 (readDualOp P k h i)))) (Ξ.reg (ι → F)).ψ = ((Ξ.reg (ι → F)).π ((Ξ.reg (ι → F)).πB (smulKron 1 (readDualOp P k h i)))) (Ξ.reg (ι → F)).ψ

The ideal dual readout is an exact mirror of itself on the register model of any bipartite auxiliary model.

theorem MIPRE.Introspection.TypedEstimates.hidingForgetTail_mapped {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 ι ℓ) (j : Fin ℓ) {R : Type u_7} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R) (z : Option ((ι → F) × (ι → F))) : fibSumIn (POVMIn.map (hidingCoarse P ↑j) M).op hidingForgetTail z = (POVMIn.map (reportedDual P (↑j) (AuxType.hide j)) M).op z

Forgetting the unused X tail of the coarse Hide measurement leaves its reported dual readout, for a POVM in any ordered ⋆-ring.

theorem MIPRE.Introspection.TypedEstimates.read_register_rigidity_alice {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 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [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 ℓ) (hMA : IsPVMIn (MA (QuestionType.hide w j, 0)).op) {δ : ℝ} (hfine : ∑ i : Option ((ι → F) × (ι → F) × (ι → F)), (Ξ.reg (ι → F)).xSqNorm ((POVMIn.map (hidingCoarse (L w) ↑j) (MA (QuestionType.hide w j, 0))).op i) (smulKron 1 (Honest.hideCoarseOp (L w) (↑j) hL i)) ≤ δ) : ∑ z : Option ((ι → F) × (ι → F)), (Ξ.reg (ι → F)).xSqNorm ((POVMIn.map (reportedDual (L w) (↑j) AuxType.read) (MA (QuestionType.read w, 0))).op z) (smulKron 1 (Honest.readDualOp (L w) (↑j) hL z)) ≤ 16 * ↑(ℓ - ↑j) ^ 2 * ↑(TypeGraph.edges E X Z ℓ).card * ε + 2 * δ

Every Read dual marginal is rigid once the corresponding hiding level is rigid. All intervening comparisons are supplied by the actual game.

theorem MIPRE.Introspection.TypedEstimates.read_register_rigidity_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] [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 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [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 ℓ) (hMA : IsPVMIn (MA (QuestionType.hide w j, 0)).op) {δ : ℝ} (hfine : ∑ i : Option ((ι → F) × (ι → F) × (ι → F)), (Ξ.reg (ι → F)).xSqNorm ((POVMIn.map (hidingCoarse (L w) ↑j) (MA (QuestionType.hide w j, 0))).op i) (smulKron 1 (Honest.hideCoarseOp (L w) (↑j) hL i)) ≤ δ) : ∑ z : Option ((ι → F) × (ι → F)), (Ξ.reg (ι → F)).xSqNorm (smulKron 1 (Honest.readDualOp (L w) (↑j) hL z)) ((POVMIn.map (reportedDual (L w) (↑j) AuxType.read) (MB (QuestionType.read w, 0))).op z) ≤ (32 * ↑(ℓ - ↑j) ^ 2 + 4) * ↑(TypeGraph.edges E X Z ℓ).card * ε + 4 * δ

The actual Read consistency loop supplies rigidity on Bob's side too.