Retaining the next hiding label without an alphabet-size loss

We first transfer the paired same-party estimate to the exact ideal mirror. Coarse-graining is then applied to cross-party PVM consistency, where positivity gives a dimension-independent contraction.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): an exact mirror is the vector identity π (πA P) ψ = π (πB R) ψ of ConditionalNormalizerMirror.lean, coarse-graining is fibSumIn, and the measurements are families and POVMs in the players' algebras. In the honest step the players' algebras are the matrices over ι → F with entries in two algebras 𝒜 and ℬ --- the register model Ξ.reg (ι → F) is one such model, and supplies the two mirrors by BipartiteModel.reg_mirror --- and an honest register operator P, a complex matrix, acts as smulKron 1 P for either player (conditionalIdeal_smulKron_one).

theorem MIPRE.Introspection.fibSumIn_smulKron_one {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] [Fintype α] [DecidableEq α] {I : Type u_3} {Z : Type u_5} [Fintype I] [DecidableEq I] [Fintype Z] [DecidableEq Z] (P : I → Matrix α α ℂ) (f : I → Z) (z : Z) : fibSumIn (fun (i : I) => smulKron 1 (P i)) f z = smulKron 1 (fibSumIn P f z)

Coarse-graining commutes with the embedding P ↦ 1 ⊗ P of register operators.

theorem MIPRE.Introspection.commute_smulKron_one {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] [Fintype α] [DecidableEq α] {P Q : Matrix α α ℂ} (h : Commute P Q) : Commute (smulKron 1 P) (smulKron 1 Q)

Commuting register operators embed as commuting operators.

theorem MIPRE.Introspection.conditionalIdeal_smulKron_one {R : Type u_1} {α : Type u_2} [Ring R] [Algebra ℂ R] [Fintype α] [DecidableEq α] {I : Type u_3} {Y : Type u_4} {Z : Type u_5} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (P : I → Matrix α α ℂ) (Q : Y → Matrix α α ℂ) (f : Y → I → Z) (p : Y × Z) : conditionalIdeal (fun (i : I) => smulKron 1 (P i)) (fun (y : Y) => smulKron 1 (Q y)) f p = smulKron 1 (conditionalIdeal P Q f p)

The conditional ideal of embedded register families is the embedded conditional ideal.

theorem MIPRE.Introspection.mirror_retained_distance_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {W : Type u_5} [Fintype I] [DecidableEq I] [Fintype W] [DecidableEq W] (hΨ : ‖Ψ.ψ‖ = 1) (P : I → 𝒜) (Q B : I → ℬ) (hP : IsPVMIn P) (hB : IsPVMIn B) (hmirror : ∀ (i : I), (Ψ.π (Ψ.πA (P i))) Ψ.ψ = (Ψ.π (Ψ.πB (Q i))) Ψ.ψ) (r : I → W) : ∑ w : W, Ψ.xSqNorm (fibSumIn P r w) (fibSumIn B r w) ≤ ∑ i : I, Ψ.snorm (Ψ.πB (B i) - Ψ.πB (Q i)) ^ 2

Exact mirror transfer followed by cross-party coarse consistency loses no constant. No same-party coarse-distance contraction is used.

theorem MIPRE.Introspection.conditional_coarse_ideal_replacement_retained {𝒞 : 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} {W : Type u_7} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hΨ : ‖Ψ.ψ‖ = 1) (M P : I → 𝒜) (R : I → ℬ) (Q : Y → 𝒜) (S : Y → ℬ) (B : Y × Z → ℬ) (f : Y → I → Z) (r : Y × Z → W) (hM : IsPVMIn M) (hP : IsPVMIn P) (hR : IsPVMIn R) (hQ : IsPVMIn Q) (hS : IsPVMIn S) (hB : IsPVMIn B) (hcA : ∀ (y : Y) (i : I), Commute (Q y) (P i)) (hcB : ∀ (y : Y) (i : I), Commute (S y) (R i)) (hmirrorP : ∀ (i : I), (Ψ.π (Ψ.πA (P i))) Ψ.ψ = (Ψ.π (Ψ.πB (R i))) Ψ.ψ) (hmirrorQ : ∀ (y : Y), (Ψ.π (Ψ.πA (Q y))) Ψ.ψ = (Ψ.π (Ψ.πB (S y))) Ψ.ψ) {α η ε : ℝ} (hfine : ∑ i : I, Ψ.xSqNorm (M i) (R i) ≤ ε) (hnorm : ∑ y : Y, Ψ.snorm (Ψ.πB (∑ z : Z, B (y, z) - S y)) ^ 2 ≤ η) (hconditional : ∑ p : Y × Z, Ψ.snorm (Ψ.πB (B p) - Ψ.πA (fibSumIn M (f p.1) p.2) * Ψ.πB (∑ z : Z, B (p.1, z))) ^ 2 ≤ α) : ∑ w : W, Ψ.xSqNorm (fibSumIn (conditionalIdeal P Q f) r w) (fibSumIn B r w) ≤ 3 * α + 3 * η + 3 * ε

The full ideal replacement remains valid after retaining any desired part of the paired conditional outcome, using primitive ideal mirrors.

theorem MIPRE.Introspection.Honest.hideNextRetain_parsed {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] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (a : ParsedAnswer (ι → F) A PauliAnswer) : hideNextRetain (TypedEstimates.hidingNextLater P k a) = TypedEstimates.hidingCoarse P (k + 1) a

The same retention map acts correctly on the entire parsed alphabet, including every malformed answer constructor.

theorem MIPRE.Introspection.Honest.hideNextRetain_mapped {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] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) {R : Type u_5} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (N : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R) (z : Option (HideLabel F ι)) : fibSumIn (POVMIn.map (TypedEstimates.hidingNextLater P k) N).op hideNextRetain z = (POVMIn.map (TypedEstimates.hidingCoarse P (k + 1)) N).op z

Retaining the next label of the paired measurement is the next coarse measurement, for a POVM in any ordered ⋆-ring.

theorem MIPRE.Introspection.Honest.hideCoarseOp_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 𝒞 (Matrix (ι → F) (ι → F) 𝒜) (Matrix (ι → F) (ι → F) ℬ)) (hΨ : ‖Ψ.ψ‖ = 1) (N : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ)) (hN : IsPVMIn N.op) (hmfine : ∀ (i : Option (HideLabel F ι)), (Ψ.π (Ψ.πA (smulKron 1 (hideCoarseOp P k h i)))) Ψ.ψ = (Ψ.π (Ψ.πB (smulKron 1 (hideCoarseOp P k h i)))) Ψ.ψ) (hmprefix : ∀ (y : Option (ι → F)), (Ψ.π (Ψ.πA (smulKron 1 (hidingPrefixOp P (k + 1) y)))) Ψ.ψ = (Ψ.π (Ψ.πB (smulKron 1 (hidingPrefixOp P (k + 1) y)))) Ψ.ψ) {δ : ℝ} (hpaired : ∑ p : Option (ι → F) × Option ((ι → F) × (ι → F) × (ι → F)), Ψ.snorm (Ψ.πB ((POVMIn.map (TypedEstimates.hidingNextLater P k) N).op p) - Ψ.π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 ι), Ψ.xSqNorm (smulKron 1 (hideCoarseOp P (k + 1) h z)) ((POVMIn.map (TypedEstimates.hidingCoarse P (k + 1)) N).op z) ≤ δ

The actual next hiding measurement is close to the next honest fine family. The paired bound is the normalizer estimate; the only state-specific inputs here are exact mirrors of the primitive ideal families.