Exact error transport through a registered auxiliary extension

Only an auxiliary register in a fixed pure state is added. The EPR register and Bob's operators remain unchanged. All identities hold for arbitrary operators and auxiliary states, without normalization or projectivity.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the auxiliary register in its fixed state is the first player's one-sided ancilla Ξ.expandA t₀, and the registered extension is the local isometry registeredExtend Ξ t₀ from the register model Ξ.reg I into (Ξ.expandA t₀).reg I: the inert embedding BipartiteModel.inertA, an old operator M becoming M ⊗ 1, followed by the reassociation regExchange. It carries the state to the state, so every error is transported exactly (LocalIsometry.stateSqNorm_of_W_ψ, xSqNorm_of_W_ψ, bornProb_of_W_ψ). The extended operator registeredExtendOp M is its ΦA, the extended measurement registeredExtendPOVM M the old one pushed forward along it, and Bob's operators are unchanged. A relabelling of the local coordinates is BipartiteModel.relabel.

def MIPRE.Introspection.registeredExtendOp {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {I : Type u_4} {T : Type u_5} [Fintype I] [Fintype T] [DecidableEq T] (M : Matrix I I 𝒜) : Matrix I I (Matrix T T 𝒜)

Extend an old operator by identity, then absorb the new register into Alice's auxiliary factor.

Equations

• MIPRE.Introspection.registeredExtendOp M = MIPRE.BipartiteModel.layerSwap (Matrix.diagonal fun (x : T) => M)

theorem MIPRE.Introspection.registeredExtendOp_eq {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {I : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (M : Matrix I I 𝒜) : registeredExtendOp M = (BipartiteModel.layerSwap.comp diagHom) M

The extension is the ⋆-homomorphism M ↦ M ⊗ 1 followed by the exchange of the layers.

theorem MIPRE.Introspection.registeredExtendOp_apply {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {I : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (M : Matrix I I 𝒜) (i j : I) : registeredExtendOp M i j = Matrix.diagonal fun (x : T) => M i j

@[simp]

theorem MIPRE.Introspection.registeredExtendOp_zero {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {I : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] : registeredExtendOp 0 = 0

theorem MIPRE.Introspection.registeredExtendOp_sub {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {I : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (M N : Matrix I I 𝒜) : registeredExtendOp (M - N) = registeredExtendOp M - registeredExtendOp N

theorem MIPRE.Introspection.registeredExtendOp_aOp {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {I : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (P : Matrix I I ℂ) : registeredExtendOp (smulKron 1 P) = smulKron 1 P

Every ideal acting on the original register is literally the same ideal tensored with the enlarged auxiliary identity.

The registered extension as a local isometry

noncomputable def MIPRE.Introspection.registeredExtend {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (t₀ : T) : (Ξ.reg I).LocalIsometry ((Ξ.expandA t₀).reg I)

The registered extension: the register model into the register model of the one-sided extension, the inert embedding of the fresh ancilla followed by its exchange with the register. The first player's operator M becomes registeredExtendOp M, the second player's are unchanged.

Equations

• MIPRE.Introspection.registeredExtend Ξ t₀ = (MIPRE.Introspection.regExchange Ξ t₀).comp ((Ξ.reg I).inertA t₀)

@[simp]

theorem MIPRE.Introspection.registeredExtend_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (t₀ : T) (M : Matrix I I 𝒜) : (registeredExtend Ξ t₀).ΦA M = registeredExtendOp M

@[simp]

theorem MIPRE.Introspection.registeredExtend_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (t₀ : T) (N : Matrix I I ℬ) : (registeredExtend Ξ t₀).ΦB N = N

theorem MIPRE.Introspection.registeredExtend_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (t₀ : T) : (registeredExtend Ξ t₀).W (Ξ.reg I).ψ = ((Ξ.expandA t₀).reg I).ψ

The registered extension carries the state to the state.

theorem MIPRE.Introspection.stateSqNorm_registeredExtendOp {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (t₀ : T) (M : Matrix I I 𝒜) : ((Ξ.expandA t₀).reg I).stateSqNorm (registeredExtendOp M) = (Ξ.reg I).stateSqNorm M

theorem MIPRE.Introspection.xSqNorm_registeredExtendOp {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (t₀ : T) (M : Matrix I I 𝒜) (N : Matrix I I ℬ) : ((Ξ.expandA t₀).reg I).xSqNorm (registeredExtendOp M) N = (Ξ.reg I).xSqNorm M N

theorem MIPRE.Introspection.snorm_bOp_registered_extVecA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (t₀ : T) (N : Matrix I I ℬ) : ((Ξ.expandA t₀).reg I).snorm (((Ξ.expandA t₀).reg I).πB N) ^ 2 = (Ξ.reg I).snorm ((Ξ.reg I).πB N) ^ 2

Bob's same-party error is unaffected by adding an auxiliary register on Alice's side, including the exact registered state reassociation.

theorem MIPRE.Introspection.bornProb_registeredExtendOp {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (t₀ : T) (M : Matrix I I 𝒜) (N : Matrix I I ℬ) : ((Ξ.expandA t₀).reg I).bornProb (registeredExtendOp M) N = (Ξ.reg I).bornProb M N

Measurements

def MIPRE.Introspection.registeredExtendPOVM {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {I : Type u_4} {T : Type u_5} {A : Type u_6} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] [Fintype A] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (M : POVMIn A (Matrix I I 𝒜)) : POVMIn A (Matrix I I (Matrix T T 𝒜))

An old measurement on the register model, tensored with the identity of the fresh ancilla and carried to the register model of the one-sided extension.

Equations

• MIPRE.Introspection.registeredExtendPOVM M = MIPRE.POVMIn.pushforward MIPRE.BipartiteModel.layerSwap ⋯ (MIPRE.Introspection.POVMIn.ampA M)

@[simp]

theorem MIPRE.Introspection.registeredExtendPOVM_mats {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {I : Type u_4} {T : Type u_5} {A : Type u_6} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] [Fintype A] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (M : POVMIn A (Matrix I I 𝒜)) (a : A) : (registeredExtendPOVM M).op a = registeredExtendOp (M.op a)

theorem MIPRE.Introspection.registeredExtendPOVM_map {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {I : Type u_4} {T : Type u_5} {A : Type u_6} {B : Type u_7} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] [Fintype A] [Fintype B] [DecidableEq B] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (M : POVMIn A (Matrix I I 𝒜)) (f : A → B) : registeredExtendPOVM (POVMIn.map f M) = POVMIn.map f (registeredExtendPOVM M)