Pauli mixing for nested registers in one ambient EPR state

This is the ambient-register form of the paper's lem:mixing. A measurement acts on V and the original ancilla, and the selected Pauli readout acts on U ⊆ V. Its extracted POVMs act on V \ U and that same ancilla. All three hypotheses and the conclusion use the one ambient EPR state. Restricting to the local register and returning to the ambient register are exact operations.

In the register model Ξ.reg (ι → F) (Phase 4 of planning/mipco-track.md): the extension of a local operator by the identity on the ambient complement is regExtendHom, the homomorphism of the register extension BipartiteModel.regExtend, which carries the state exactly.

def MIPRE.Introspection.ambientOperator {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype F] [DecidableEq F] {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (V : Finset ι) (M : Matrix (↥V → F) (↥V → F) 𝒜) : Matrix (ι → F) (ι → F) 𝒜

Extend an operator on V and the ancilla by identity on V's ambient complement.

Equations

• MIPRE.Introspection.ambientOperator V M = (MIPRE.Introspection.regExtendHom (MIPRE.Introspection.ambientSplit V)) M

noncomputable def MIPRE.Introspection.ambientReadout {ι : 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 ℂ 𝒜] (U V : Finset ι) (hUV : U ⊆ V) (w : (Fin (Fintype.card ↥U) → F) → Matrix (Fin (Fintype.card ↥U) → F) (Fin (Fintype.card ↥U) → F) ℂ) (L : (Fin (Fintype.card ↥U) → F) →ₗ[F] Fin (Fintype.card ↥U) → F) (y : Fin (Fintype.card ↥U) → F) : Matrix (ι → F) (ι → F) 𝒜

The selected readout, embedded into the original ambient space.

Equations

• MIPRE.Introspection.ambientReadout U V hUV w L y = MIPRE.Introspection.ambientOperator V (MIPRE.Introspection.registerReadout (MIPRE.Introspection.coordinateSplit U V hUV) w L y)

theorem MIPRE.Introspection.stateSqNorm_ambientOperator {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (V : Finset ι) (M : Matrix (↥V → F) (↥V → F) 𝒜) : (Ξ.reg (ι → F)).stateSqNorm ((regExtendHom (ambientSplit V)) M) = (Ξ.reg (↥V → F)).stateSqNorm M

A local operator extended to the ambient register has its state error on the local EPR factor.

noncomputable def MIPRE.Introspection.ambientMarginalError {ι : 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] {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (U V : Finset ι) (hUV : U ⊆ V) (L : CL.RegLinear F U) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (Fin (Fintype.card ↥U) → F) × A → Matrix (↥V → F) (↥V → F) 𝒜) : ℝ

Ambient consistency of the first outcome with the selected Z readout.

Equations

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

noncomputable def MIPRE.Introspection.ambientCommutatorError {ι : 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] {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (U V : Finset ι) (hUV : U ⊆ V) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (Fin (Fintype.card ↥U) → F) × A → Matrix (↥V → F) (↥V → F) 𝒜) (w : (Fin (Fintype.card ↥U) → F) → Matrix (Fin (Fintype.card ↥U) → F) (Fin (Fintype.card ↥U) → F) ℂ) (L : (Fin (Fintype.card ↥U) → F) →ₗ[F] Fin (Fintype.card ↥U) → F) : ℝ

Ambient commutation with a selected Pauli readout.

Equations

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

theorem MIPRE.Introspection.ambientMarginalError_eq {ι : 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 ℂ ℬ] (U V : Finset ι) (hUV : U ⊆ V) (L : CL.RegLinear F U) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (Fin (Fintype.card ↥U) → F) × A → Matrix (↥V → F) (↥V → F) 𝒜) : ambientMarginalError U V hUV L Ξ M = registerMarginalError (coordinateSplit U V hUV) (coordinateLinear L) Ξ M

Consistency on the ambient state is exactly consistency on the local EPR factor.

theorem MIPRE.Introspection.ambientCommutatorError_eq {ι : 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 ℂ ℬ] (U V : Finset ι) (hUV : U ⊆ V) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (Fin (Fintype.card ↥U) → F) × A → Matrix (↥V → F) (↥V → F) 𝒜) (w : (Fin (Fintype.card ↥U) → F) → Matrix (Fin (Fintype.card ↥U) → F) (Fin (Fintype.card ↥U) → F) ℂ) (L : (Fin (Fintype.card ↥U) → F) →ₗ[F] Fin (Fintype.card ↥U) → F) : ambientCommutatorError U V hUV Ξ M w L = registerCommutatorError (coordinateSplit U V hUV) Ξ M w L

Commutation on the ambient state is exactly commutation on the local EPR factor.

theorem MIPRE.Introspection.exists_ambient_pauli_mixing {ι : 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 𝒜] {X : Type u_7} [Fintype X] (D : X → ℝ) (hD0 : ∀ (x : X), 0 ≤ D x) (hD1 : ∑ x : X, D x = 1) (U V : X → Finset ι) (hUV : ∀ (x : X), U x ⊆ V x) (L : (x : X) → CL.RegLinear F (U x)) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (M : (x : X) → POVMIn ((Fin (Fintype.card ↥(U x)) → F) × A) (Matrix (↥(V x) → F) (↥(V x) → F) 𝒜)) (hM : ∀ (x : X), IsPVMIn (M x).op) {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hmarg : ∑ x : X, D x * ambientMarginalError (U x) (V x) ⋯ (L x) Ξ (M x).op ≤ ε) (hZ : ∑ x : X, D x * ambientCommutatorError (U x) (V x) ⋯ Ξ (M x).op Weyl.wZ LinearMap.id ≤ ε) (hX : ∑ x : X, D x * ambientCommutatorError (U x) (V x) ⋯ Ξ (M x).op Weyl.wX (CL.lperp (coordinateLinear (L x))) ≤ ε) : ∃ (Q : (x : X) → (Fin (Fintype.card ↥(U x)) → F) → POVMIn A (Matrix (↥(V x \ U x) → F) (↥(V x \ U x) → F) 𝒜)), ∑ x : X, D x * ∑ p : (Fin (Fintype.card ↥(U x)) → F) × A, (Ξ.reg (ι → F)).stateSqNorm (ambientOperator (V x) ((M x).op p) - ambientOperator (V x) ((regSplitHom (coordinateSplit (U x) (V x) ⋯)) (smulKron ((Q x p.1).op p.2) (Weyl.synOf Weyl.wZ (⇑(coordinateLinear (L x))) p.1)))) ≤ 56 * √ε

Ambient Pauli mixing. The finite-set register inclusions, the CL linear maps, and the one global EPR state are supplied directly. The output measurements have precisely the local residual register as support. All answer values, including those outside the linear map's range, occur in the sums; the error is at most 56 sqrt ε.