The next hiding step on an EPR seed with arbitrary auxiliaries

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 an arbitrary model Ξ, whose players hold the matrices over ι → F with entries in Ξ's algebras, and an honest register operator P, a complex matrix, acts as smulKron 1 P for either player. The honest operators are symmetric, so the mirror identity of the register model (BipartiteModel.reg_mirror) makes each of them an exact mirror of itself, and the step is hideCoarseOp_step_of_normalizer in the register model. Register families are embedded, with their coarse-grainings and conditional ideals, by fibSumIn_smulKron_one and conditionalIdeal_smulKron_one (ConditionalNormalizerStep.lean).

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

Exact ideal mirrors persist with any bipartite auxiliary model.

theorem MIPRE.Introspection.Honest.hidingPrefixOp_registerState_mirror {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (P : CL.CLFun F ι ℓ) (k : ℕ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (y : Option (ι → F)) : ((Ξ.reg (ι → F)).π ((Ξ.reg (ι → F)).πA (smulKron 1 (hidingPrefixOp P k y)))) (Ξ.reg (ι → F)).ψ = ((Ξ.reg (ι → F)).π ((Ξ.reg (ι → F)).πB (smulKron 1 (hidingPrefixOp P k y)))) (Ξ.reg (ι → F)).ψ

theorem MIPRE.Introspection.Honest.hidingPrefixOp_aux_commute {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {R : Type u_8} [Ring R] [Algebra ℂ R] (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) (y : Option (ι → F)) (i : Option (HideLabel F ι)) : Commute (smulKron 1 (hidingPrefixOp P (k + 1) y)) (smulKron 1 (hideCoarseOp P k h i))

The next honest prefix commutes with the current coarse Hide measurement, both embedded in the matrices over any algebra.

theorem MIPRE.Introspection.Honest.hideCoarseOp_aux_step_of_normalizer {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PauliAnswer : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype PauliAnswer] {ℓ : ℕ} {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (P : CL.CLFun F ι ℓ) (k : ℕ) (hk : k + 1 < ℓ) (h : P.SupportedOn Finset.univ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (N : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ)) (hN : IsPVMIn N.op) {δ : ℝ} (hpaired : ∑ p : Option (ι → F) × Option ((ι → F) × (ι → F) × (ι → F)), (Ξ.reg (ι → F)).snorm ((Ξ.reg (ι → F)).πB ((POVMIn.map (TypedEstimates.hidingNextLater P k) N).op p) - (Ξ.reg (ι → F)).πB (conditionalIdeal (fun (i : Option (HideLabel F ι)) => smulKron 1 (hideCoarseOp P k h i)) (fun (y : Option (ι → F)) => smulKron 1 (hidingPrefixOp P (k + 1) y)) (TypedEstimates.hidingNextGuarded P k) p)) ^ 2 ≤ δ) : ∑ z : Option (HideLabel F ι), (Ξ.reg (ι → F)).xSqNorm (smulKron 1 (hideCoarseOp P (k + 1) h z)) ((POVMIn.map (TypedEstimates.hidingCoarse P (k + 1)) N).op z) ≤ δ

The paired normalizer bound implies rigidity of the actual next coarse Hide measurement on the full seed/auxiliary carrier. All ideal mirrors and conditional product identities are supplied by the honest construction.