Exact mirror transfer for the conditional ideal family

Primitive fine and prefix mirrors imply the mirror identity for the keyed conditional ideal family. Consequently the one-party replacement estimate is also the cross-party error needed by the hiding induction.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): an exact mirror of the first player's operator P by the second player's R is the identity of vectors π (πA P) ψ = π (πB R) ψ, the form in which the register model supplies it (BipartiteModel.reg_mirror, mirror_expand); in the tensor-product model it is aOp P *ᵥ ψ = bOp R *ᵥ ψ. Coarse-graining is fibSumIn, and A ⊗ B is πA A * πB B.

theorem MIPRE.Introspection.fibSum_mirror {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {Z : Type u_6} [Fintype I] [DecidableEq I] [Fintype Z] [DecidableEq Z] (P : I → 𝒜) (R : I → ℬ) (h : ∀ (i : I), (Ψ.π (Ψ.πA (P i))) Ψ.ψ = (Ψ.π (Ψ.πB (R i))) Ψ.ψ) (f : I → Z) (z : Z) : (Ψ.π (Ψ.πA (fibSumIn P f z))) Ψ.ψ = (Ψ.π (Ψ.πB (fibSumIn R f z))) Ψ.ψ

Exact mirrors are preserved by coarse-graining both families along the same map.

theorem MIPRE.Introspection.conditionalIdeal_mirror {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {Y : Type u_5} {Z : Type u_6} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (P : I → 𝒜) (R : I → ℬ) (Q : Y → 𝒜) (S : Y → ℬ) (f : Y → I → Z) (hP : ∀ (i : I), (Ψ.π (Ψ.πA (P i))) Ψ.ψ = (Ψ.π (Ψ.πB (R i))) Ψ.ψ) (hQ : ∀ (y : Y), (Ψ.π (Ψ.πA (Q y))) Ψ.ψ = (Ψ.π (Ψ.πB (S y))) Ψ.ψ) (hc : ∀ (y : Y) (i : I), Commute (S y) (R i)) (p : Y × Z) : (Ψ.π (Ψ.πA (conditionalIdeal P Q f p))) Ψ.ψ = (Ψ.π (Ψ.πB (conditionalIdeal R S f p))) Ψ.ψ

Mirrors reverse multiplication order; commutation of the ideal prefix and fine projectors restores the order defining the conditional ideal.

theorem MIPRE.Introspection.xSqNorm_eq_bOp_distance_of_mirror {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (P : 𝒜) (Q B : ℬ) (h : (Ψ.π (Ψ.πA P)) Ψ.ψ = (Ψ.π (Ψ.πB Q)) Ψ.ψ) : Ψ.xSqNorm P B = Ψ.snorm (Ψ.πB B - Ψ.πB Q) ^ 2

An exact mirror changes a cross-party distance into a same-party distance.

theorem MIPRE.Introspection.conditional_coarse_ideal_replacement_mirror {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {Y : Type u_5} {Z : Type u_6} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hΨ : ‖Ψ.ψ‖ = 1) (M P : I → 𝒜) (R : I → ℬ) (Q : Y → 𝒜) (S : Y → ℬ) (B : Y × Z → ℬ) (f : Y → I → Z) (hM : IsPVMIn M) (hR : IsPVMIn R) (hS : IsPVMIn S) (hc : ∀ (y : Y) (i : I), Commute (S y) (R i)) (hP : ∀ (i : I), (Ψ.π (Ψ.πA (P i))) Ψ.ψ = (Ψ.π (Ψ.πB (R i))) Ψ.ψ) (hQ : ∀ (y : Y), (Ψ.π (Ψ.πA (Q y))) Ψ.ψ = (Ψ.π (Ψ.πB (S y))) Ψ.ψ) {α η ε : ℝ} (hfine : ∑ i : I, Ψ.xSqNorm (M i) (R i) ≤ ε) (hnorm : ∑ y : Y, Ψ.xSqNorm (Q y) (∑ z : Z, B (y, z)) ≤ η) (hconditional : ∑ p : Y × Z, Ψ.snorm (Ψ.πB (B p) - Ψ.πA (fibSumIn M (f p.1) p.2) * Ψ.πB (∑ z : Z, B (p.1, z))) ^ 2 ≤ α) : ∑ p : Y × Z, Ψ.xSqNorm (conditionalIdeal P Q f p) (B p) ≤ 3 * α + 3 * η + 3 * ε

The conditional replacement gives the cross-party ideal estimate whenever the primitive ideal families have their exact EPR mirrors.