Pauli mixing in the original local register

The basis equivalence explicitly splits the retained coordinates from the local complement. Hypotheses and the conclusion are stated on the original EPR state, and the output POVMs act only on that local complement and the original ancilla.

In the register model Ξ.reg I (Phase 4 of planning/mipco-track.md), the split of the register along e : I ≃ (Fin n → F) × R is the local isometry BipartiteModel.regSplit, whose homomorphism regSplitHom e reads a block matrix over the coordinates of block matrices over the complement as a block matrix over I, with inverse regSplitInvHom e.

noncomputable def MIPRE.Introspection.registerReadout {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {I : Type u_2} {R : Type u_3} [Fintype I] [Fintype R] [DecidableEq R] {n : ℕ} {𝒜 : Type u_6} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (e : I ≃ (Fin n → F) × R) (w : (Fin n → F) → Matrix (Fin n → F) (Fin n → F) ℂ) (L : (Fin n → F) →ₗ[F] Fin n → F) (y : Fin n → F) : Matrix I I 𝒜

Read a Pauli linear map on the selected coordinates of the original register.

Equations

• MIPRE.Introspection.registerReadout e w L y = (MIPRE.Introspection.regSplitHom e) (MIPRE.smulKron 1 (MIPRE.Weyl.synOf w (⇑L) y))

theorem MIPRE.Introspection.stateSqNorm_split_original {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {I : Type u_2} {R : Type u_3} [Fintype I] [DecidableEq I] [Fintype R] [DecidableEq R] {n : ℕ} {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] (e : I ≃ (Fin n → F) × R) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : Matrix I I 𝒜) : (Ξ.reg I).stateSqNorm M = ((Ξ.reg R).reg (Fin n → F)).stateSqNorm ((regSplitInvHom e) M)

Express any local operator in split coordinates without changing its state error.

noncomputable def MIPRE.Introspection.registerMarginalError {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {I : Type u_2} {R : Type u_3} {A : Type u_4} [Fintype I] [DecidableEq I] [Fintype R] [DecidableEq R] [Fintype A] {n : ℕ} {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (e : I ≃ (Fin n → F) × R) (L : (Fin n → F) →ₗ[F] Fin n → F) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (Fin n → F) × A → Matrix I I 𝒜) : ℝ

The first marginal consistency error in the original coordinates.

Equations

• MIPRE.Introspection.registerMarginalError e L Ξ M = ∑ y : Fin n → F, (Ξ.reg I).stateSqNorm (∑ a : A, M (y, a) - MIPRE.Introspection.registerReadout e MIPRE.Weyl.wZ L y)

noncomputable def MIPRE.Introspection.registerCommutatorError {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {I : Type u_2} {R : Type u_3} {A : Type u_4} [Fintype I] [DecidableEq I] [Fintype R] [DecidableEq R] [Fintype A] {n : ℕ} {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (e : I ≃ (Fin n → F) × R) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (Fin n → F) × A → Matrix I I 𝒜) (w : (Fin n → F) → Matrix (Fin n → F) (Fin n → F) ℂ) (L : (Fin n → F) →ₗ[F] Fin n → F) : ℝ

The readout commutation error in the original coordinates.

Equations

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

theorem MIPRE.Introspection.registerMarginalError_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {I : Type u_2} {R : Type u_3} {A : Type u_4} [Fintype I] [DecidableEq I] [Fintype R] [DecidableEq R] [Fintype A] [DecidableEq A] {n : ℕ} {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] (e : I ≃ (Fin n → F) × R) (L : (Fin n → F) →ₗ[F] Fin n → F) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (Fin n → F) × A → Matrix I I 𝒜) : registerMarginalError e L Ξ M = readoutMarginalError L ((Ξ.reg R).reg (Fin n → F)) fun (p : (Fin n → F) × A) => (regSplitInvHom e) (M p)

theorem MIPRE.Introspection.registerCommutatorError_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {I : Type u_2} {R : Type u_3} {A : Type u_4} [Fintype I] [DecidableEq I] [Fintype R] [DecidableEq R] [Fintype A] [DecidableEq A] {n : ℕ} {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] (e : I ≃ (Fin n → F) × R) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (Fin n → F) × A → Matrix I I 𝒜) (w : (Fin n → F) → Matrix (Fin n → F) (Fin n → F) ℂ) (L : (Fin n → F) →ₗ[F] Fin n → F) : registerCommutatorError e Ξ M w L = readoutCommutatorError ((Ξ.reg R).reg (Fin n → F)) (fun (p : (Fin n → F) × A) => (regSplitInvHom e) (M p)) w L

theorem MIPRE.Introspection.exists_register_mixing_sqrt {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {A : Type u_4} [Fintype A] [DecidableEq A] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {X : Type u_8} [Fintype X] {n : X → ℕ} {I : X → Type u_9} {R : X → Type u_10} [(x : X) → Fintype (I x)] [(x : X) → DecidableEq (I x)] [(x : X) → Fintype (R x)] [(x : X) → DecidableEq (R x)] [∀ (x : X), Nonempty (R x)] (D : X → ℝ) (hD0 : ∀ (x : X), 0 ≤ D x) (hD1 : ∑ x : X, D x = 1) (e : (x : X) → I x ≃ (Fin (n x) → F) × R x) (L : (x : X) → (Fin (n x) → F) →ₗ[F] Fin (n x) → F) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (M : (x : X) → POVMIn ((Fin (n x) → F) × A) (Matrix (I x) (I x) 𝒜)) (hM : ∀ (x : X), IsPVMIn (M x).op) {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hmarg : ∑ x : X, D x * registerMarginalError (e x) (L x) Ξ (M x).op ≤ ε) (hZ : ∑ x : X, D x * registerCommutatorError (e x) Ξ (M x).op Weyl.wZ LinearMap.id ≤ ε) (hX : ∑ x : X, D x * registerCommutatorError (e x) Ξ (M x).op Weyl.wX (CL.lperp (L x)) ≤ ε) : ∃ (Q : (x : X) → (Fin (n x) → F) → POVMIn A (Matrix (R x) (R x) 𝒜)), ∑ x : X, D x * ∑ p : (Fin (n x) → F) × A, (Ξ.reg (I x)).stateSqNorm ((M x).op p - (regSplitHom (e x)) (smulKron ((Q x p.1).op p.2) (Weyl.synOf Weyl.wZ (⇑(L x)) p.1))) ≤ 56 * √ε

Pauli mixing on the original registers, with question-dependent coordinate splits. The conclusion supplies genuine POVMs on the local complement, with no ambient complement adjoined to their support and no dimension factor in the error.