One product-form induction step from the coarse joint measurements

The two commutators needed by Pauli mixing are derived from the tested marginals of actual projective measurements on the other party. Coarse-graining is performed before applying the commutation analysis. The error does not depend on the size of a coarse-graining fibre.

The final theorem constructs the residual POVMs on V \ U, from averaged cross-party errors on one ambient EPR state. Identifying these measurements with the prefix-conditioned introspection strategy is a separate obligation.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md). The coarse joint measurement is a projective measurement in the other player's algebra, and the ambient EPR state is the register model Ξ.reg (ι → F): a local measurement on V is a POVM of V → F block matrices over the first player's algebra of Ξ, carried to the ambient register by ambientOperator, and the residual POVMs are V \ U → F block matrices over that algebra, placed beside the selected Pauli readout by regSplitHom.

def MIPRE.Introspection.coarseJointLeftError {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {C : Type u_5} {O : Type u_6} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] [Fintype O] (M : POVMIn A 𝒜) (B : POVMIn O ℬ) (f : O → A × C) : ℝ

Consistency with the first marginal of an actual coarse joint measurement.

Equations

• MIPRE.Introspection.coarseJointLeftError Ψ M B f = ∑ a : A, Ψ.xSqNorm (M.op a) (∑ c : C, (MIPRE.POVMIn.map f B).op (a, c))

def MIPRE.Introspection.coarseJointRightError {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {C : Type u_5} {O : Type u_6} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] [Fintype O] (N : POVMIn C 𝒜) (B : POVMIn O ℬ) (f : O → A × C) : ℝ

Consistency with the second marginal of the same coarse joint measurement.

Equations

• MIPRE.Introspection.coarseJointRightError Ψ N B f = ∑ c : C, Ψ.xSqNorm (N.op c) (∑ a : A, (MIPRE.POVMIn.map f B).op (a, c))

theorem MIPRE.Introspection.coarseJointLeftError_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {C : Type u_5} {O : Type u_6} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] [Fintype O] (M : POVMIn A 𝒜) (B : POVMIn O ℬ) (f : O → A × C) : 0 ≤ coarseJointLeftError Ψ M B f

theorem MIPRE.Introspection.coarseJointRightError_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {C : Type u_5} {O : Type u_6} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] [Fintype O] (N : POVMIn C 𝒜) (B : POVMIn O ℬ) (f : O → A × C) : 0 ≤ coarseJointRightError Ψ N B f

theorem MIPRE.Introspection.coarse_joint_commutator_bound {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {C : Type u_5} {O : Type u_6} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] [Fintype O] (M : POVMIn A 𝒜) (N : POVMIn C 𝒜) (B : POVMIn O ℬ) (hB : IsPVMIn B.op) (f : O → A × C) : ∑ a : A, ∑ c : C, Ψ.stateSqNorm (M.op a * N.op c - N.op c * M.op a) ≤ 16 * (coarseJointLeftError Ψ M B f + coarseJointRightError Ψ N B f)

The coarse joint measurement is used directly. In particular this theorem does not coarse-grain an already established commutator estimate.

theorem MIPRE.Introspection.ambientOperator_isPVM {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (V : Finset ι) {M : A → Matrix (↥V → F) (↥V → F) 𝒜} (hM : IsPVMIn M) : IsPVMIn fun (a : A) => ambientOperator V (M a)

Embedding in the ambient register preserves the projective measurement.

theorem MIPRE.Introspection.ambientReadout_isPVM {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (U V : Finset ι) (hUV : U ⊆ V) (w : (Fin (Fintype.card ↥U) → F) → Matrix (Fin (Fintype.card ↥U) → F) (Fin (Fintype.card ↥U) → F) ℂ) (hw : Weyl.IsWeylFamily w) (L : (Fin (Fintype.card ↥U) → F) →ₗ[F] Fin (Fintype.card ↥U) → F) : IsPVMIn (ambientReadout U V hUV w L)

Projectivity of a selected linear Pauli readout in the original register.

def MIPRE.Introspection.ambientProjectivePOVM {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (V : Finset ι) (M : POVMIn A (Matrix (↥V → F) (↥V → F) 𝒜)) (hM : IsPVMIn M.op) : POVMIn A (Matrix (ι → F) (ι → F) 𝒜)

The actual ambient POVM of a projective local measurement.

Equations

• MIPRE.Introspection.ambientProjectivePOVM V M hM = ⋯.toPOVMIn

@[simp]

theorem MIPRE.Introspection.ambientProjectivePOVM_mats {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (V : Finset ι) (M : POVMIn A (Matrix (↥V → F) (↥V → F) 𝒜)) (hM : IsPVMIn M.op) (a : A) : (ambientProjectivePOVM V M hM).op a = ambientOperator V (M.op a)

noncomputable def MIPRE.Introspection.ambientReadoutPOVM {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (U V : Finset ι) (hUV : U ⊆ V) (w : (Fin (Fintype.card ↥U) → F) → Matrix (Fin (Fintype.card ↥U) → F) (Fin (Fintype.card ↥U) → F) ℂ) (hw : Weyl.IsWeylFamily w) (L : (Fin (Fintype.card ↥U) → F) →ₗ[F] Fin (Fintype.card ↥U) → F) : POVMIn (Fin (Fintype.card ↥U) → F) (Matrix (ι → F) (ι → F) 𝒜)

The selected Pauli readout as a normalized positive measurement.

Equations

• MIPRE.Introspection.ambientReadoutPOVM U V hUV w hw L = ⋯.toPOVMIn

@[simp]

theorem MIPRE.Introspection.ambientReadoutPOVM_mats {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (U V : Finset ι) (hUV : U ⊆ V) (w : (Fin (Fintype.card ↥U) → F) → Matrix (Fin (Fintype.card ↥U) → F) (Fin (Fintype.card ↥U) → F) ℂ) (hw : Weyl.IsWeylFamily w) (L : (Fin (Fintype.card ↥U) → F) →ₗ[F] Fin (Fintype.card ↥U) → F) (y : Fin (Fintype.card ↥U) → F) : (ambientReadoutPOVM U V hUV w hw L).op y = ambientReadout U V hUV w L y

noncomputable def MIPRE.Introspection.productStageTestError {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {B : Type u_7} {C : Type u_8} [Fintype B] [Fintype C] (U V : Finset ι) (hUV : U ⊆ V) (L : CL.RegLinear F U) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : POVMIn ((Fin (Fintype.card ↥U) → F) × A) (Matrix (↥V → F) (↥V → F) 𝒜)) (hM : IsPVMIn M.op) (BZ : POVMIn B (Matrix (ι → F) (ι → F) ℬ)) (BX : POVMIn C (Matrix (ι → F) (ι → F) ℬ)) (fZ : B → ((Fin (Fintype.card ↥U) → F) × A) × (Fin (Fintype.card ↥U) → F)) (fX : C → ((Fin (Fintype.card ↥U) → F) × A) × (Fin (Fintype.card ↥U) → F)) (R : POVMIn (Fin (Fintype.card ↥U) → F) (Matrix (ι → F) (ι → F) ℬ)) : ℝ

The six cross-party errors used in one product-form stage: two sampling marginal comparisons, and the two marginal comparisons for each coarse joint measurement. Every summand is evaluated on the same original ambient state.

Equations

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

theorem MIPRE.Introspection.productStage_mixing_premises {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {B : Type u_7} {C : Type u_8} [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] (U V : Finset ι) (hUV : U ⊆ V) (L : CL.RegLinear F U) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : POVMIn ((Fin (Fintype.card ↥U) → F) × A) (Matrix (↥V → F) (↥V → F) 𝒜)) (hM : IsPVMIn M.op) (BZ : POVMIn B (Matrix (ι → F) (ι → F) ℬ)) (BX : POVMIn C (Matrix (ι → F) (ι → F) ℬ)) (hBZ : IsPVMIn BZ.op) (hBX : IsPVMIn BX.op) (fZ : B → ((Fin (Fintype.card ↥U) → F) × A) × (Fin (Fintype.card ↥U) → F)) (fX : C → ((Fin (Fintype.card ↥U) → F) × A) × (Fin (Fintype.card ↥U) → F)) (R : POVMIn (Fin (Fintype.card ↥U) → F) (Matrix (ι → F) (ι → F) ℬ)) : ambientMarginalError U V hUV L Ξ M.op ≤ 16 * productStageTestError U V hUV L Ξ M hM BZ BX fZ fX R ∧ ambientCommutatorError U V hUV Ξ M.op Weyl.wZ LinearMap.id ≤ 16 * productStageTestError U V hUV L Ξ M hM BZ BX fZ fX R ∧ ambientCommutatorError U V hUV Ξ M.op Weyl.wX (CL.lperp (coordinateLinear L)) ≤ 16 * productStageTestError U V hUV L Ξ M hM BZ BX fZ fX R

All three analytic premises of mixing follow from the actual coarse joint measurements and a common opposite-party sampling marginal.

theorem MIPRE.Introspection.exists_product_stage_of_coarse_tests {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {B : Type u_7} {C : Type u_8} [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] {J : Type u_9} [Fintype J] (D : J → ℝ) (hD0 : ∀ (j : J), 0 ≤ D j) (hD1 : ∑ j : J, D j = 1) (U V : J → Finset ι) (hUV : ∀ (j : J), U j ⊆ V j) (L : (j : J) → CL.RegLinear F (U j)) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (M : (j : J) → POVMIn ((Fin (Fintype.card ↥(U j)) → F) × A) (Matrix (↥(V j) → F) (↥(V j) → F) 𝒜)) (hM : ∀ (j : J), IsPVMIn (M j).op) (BZ : J → POVMIn B (Matrix (ι → F) (ι → F) ℬ)) (BX : J → POVMIn C (Matrix (ι → F) (ι → F) ℬ)) (hBZ : ∀ (j : J), IsPVMIn (BZ j).op) (hBX : ∀ (j : J), IsPVMIn (BX j).op) (fZ : (j : J) → B → ((Fin (Fintype.card ↥(U j)) → F) × A) × (Fin (Fintype.card ↥(U j)) → F)) (fX : (j : J) → C → ((Fin (Fintype.card ↥(U j)) → F) × A) × (Fin (Fintype.card ↥(U j)) → F)) (R : (j : J) → POVMIn (Fin (Fintype.card ↥(U j)) → F) (Matrix (ι → F) (ι → F) ℬ)) {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : 16 * ε ≤ 1) (htests : ∑ j : J, D j * productStageTestError (U j) (V j) ⋯ (L j) Ξ (M j) ⋯ (BZ j) (BX j) (fZ j) (fX j) (R j) ≤ ε) : ∃ (Q : (j : J) → (Fin (Fintype.card ↥(U j)) → F) → POVMIn A (Matrix (↥(V j \ U j) → F) (↥(V j \ U j) → F) 𝒜)), ∑ j : J, D j * ∑ p : (Fin (Fintype.card ↥(U j)) → F) × A, (Ξ.reg (ι → F)).stateSqNorm (ambientOperator (V j) ((M j).op p) - ambientOperator (V j) ((regSplitHom (coordinateSplit (U j) (V j) ⋯)) (smulKron ((Q j p.1).op p.2) (Weyl.synOf Weyl.wZ (⇑(coordinateLinear (L j))) p.1)))) ≤ 224 * √ε

One product-form extraction stage. The input consists of the actual projective local measurement, two opposite-party projective measurements with explicit coarse outcome maps, and the sampling marginal. Small average test errors construct the next POVMs on exactly V \ U and the original ancilla. Neither commutation nor the product-form conclusion is assumed.