Reassembly in the original EPR-register ordering

The added register belongs to Alice's auxiliary space. The shared state is exactly the original EPR factor tensored with that extended auxiliary state. These definitions construct the actual strategy on finite registers and preserve all nonselected measurements under the displayed reassociation.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the replacement lives on the one-sided extension (Ξ.reg I).expandA t₀ of the register model, and the reassociation is the local isometry regExchange onto (Ξ.expandA t₀).reg I, which exchanges the fresh ancilla with the register on the first player's side (BipartiteModel.exchange).

@[reducible, inline]

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

The reassociation: the fresh ancilla of the register model, exchanged with the register, is an ancilla of the auxiliary model.

Equations

• MIPRE.Introspection.regExchange Ξ t₀ = MIPRE.BipartiteModel.exchange t₀ (MIPRE.Introspection.registerEPR I)

theorem MIPRE.Introspection.regExchange_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_9} {T : Type u_10} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (t₀ : T) : (regExchange Ξ t₀).W ((Ξ.reg I).expandA t₀).ψ = ((Ξ.expandA t₀).reg I).ψ

Reassociation places the fresh fixed ancilla entirely in the auxiliary state and leaves the EPR factor literally unchanged.

def MIPRE.Introspection.registeredReplacement {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {X : Type u_4} {A : Type u_6} {I : Type u_9} {T : Type u_10} [DecidableEq X] [Fintype A] [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (MA : X → POVMIn A (Matrix I I 𝒜)) (q : X) (R : POVMIn A (Matrix T T (Matrix I I 𝒜))) : X → POVMIn A (Matrix I I (Matrix T T 𝒜))

The new actual question-indexed family in the original register-first ordering.

Equations

• MIPRE.Introspection.registeredReplacement MA q R x = MIPRE.POVMIn.pushforward MIPRE.BipartiteModel.layerSwap ⋯ (MIPRE.Introspection.replaceExtended MA q R x)

@[simp]

theorem MIPRE.Introspection.registeredReplacement_at {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {X : Type u_4} {A : Type u_6} {I : Type u_9} {T : Type u_10} [Fintype X] [DecidableEq X] [Fintype A] [DecidableEq A] [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (MA : X → POVMIn A (Matrix I I 𝒜)) (q : X) (R : POVMIn A (Matrix T T (Matrix I I 𝒜))) : registeredReplacement MA q R q = POVMIn.pushforward BipartiteModel.layerSwap ⋯ R

theorem MIPRE.Introspection.registeredReplacement_other {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {X : Type u_4} {A : Type u_6} {I : Type u_9} {T : Type u_10} [Fintype X] [DecidableEq X] [Fintype A] [DecidableEq A] [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (MA : X → POVMIn A (Matrix I I 𝒜)) (q x : X) (R : POVMIn A (Matrix T T (Matrix I I 𝒜))) (hx : x ≠ q) : registeredReplacement MA q R x = POVMIn.pushforward BipartiteModel.layerSwap ⋯ (POVMIn.ampA (MA x))

theorem MIPRE.Introspection.registeredReplacement_isPVM {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {X : Type u_4} {A : Type u_6} {I : Type u_9} {T : Type u_10} [Fintype X] [DecidableEq X] [Fintype A] [DecidableEq A] [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (MA : X → POVMIn A (Matrix I I 𝒜)) (q : X) (R : POVMIn A (Matrix T T (Matrix I I 𝒜))) (hMA : ∀ (x : X), IsPVMIn (MA x).op) (hR : IsPVMIn R.op) (x : X) : IsPVMIn (registeredReplacement MA q R x).op

theorem MIPRE.Introspection.registeredReplacement_value_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} {I : Type u_9} {T : Type u_10} [Fintype X] [DecidableEq X] [Fintype Y] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] (G : Game X Y A B) (t₀ : T) (MA : X → POVMIn A (Matrix I I 𝒜)) (MB : Y → POVMIn B (Matrix I I ℬ)) (q : X) (R : POVMIn A (Matrix T T (Matrix I I 𝒜))) : ((Ξ.expandA t₀).reg I).povmValue G (registeredReplacement MA q R) MB = ((Ξ.reg I).expandA t₀).povmValue G (replaceExtended MA q R) MB

The registered replacement and its unreassociated version have exactly the same value, for every game.

theorem MIPRE.Introspection.norm_reg_expandA_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_9} {T : Type u_10} [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] [Nonempty I] (hΞ : ‖Ξ.ψ‖ = 1) (t₀ : T) : ‖((Ξ.expandA t₀).reg I).ψ‖ = 1

The fixed auxiliary extension is normalized, hence gives the actual normalized EPR-plus-auxiliary state of the next strategy.

def MIPRE.Introspection.registeredReplacementStrategy {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} {I : Type u_9} {T : Type u_10} [Fintype X] [DecidableEq X] [Fintype Y] [Fintype A] [DecidableEq A] [Fintype B] [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] [Nonempty I] (G : Game X Y A B) (hΞ : ‖Ξ.ψ‖ = 1) (t₀ : T) (MA : X → POVMIn A (Matrix I I 𝒜)) (MB : Y → POVMIn B (Matrix I I ℬ)) (q : X) (R : POVMIn A (Matrix T T (Matrix I I 𝒜))) (hMA : ∀ (x : X), IsPVMIn (MA x).op) (hMB : ∀ (y : Y), IsPVMIn (MB y).op) (hR : IsPVMIn R.op) : ((Ξ.expandA t₀).reg I).ProjStrat G

A concrete legal strategy on the new register state.

Equations

• MIPRE.Introspection.registeredReplacementStrategy Ξ G hΞ t₀ MA MB q R hMA hMB hR = { PA := MIPRE.Introspection.registeredReplacement MA q R, PB := MB, projA := ⋯, projB := hMB, ψ_unit := ⋯ }

theorem MIPRE.Introspection.registeredReplacementStrategy_value {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} {I : Type u_9} {T : Type u_10} [Fintype X] [DecidableEq X] [Fintype Y] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] [Nonempty I] (G : Game X Y A B) (hΞ : ‖Ξ.ψ‖ = 1) (t₀ : T) (MA : X → POVMIn A (Matrix I I 𝒜)) (MB : Y → POVMIn B (Matrix I I ℬ)) (q : X) (R : POVMIn A (Matrix T T (Matrix I I 𝒜))) (hMA : ∀ (x : X), IsPVMIn (MA x).op) (hMB : ∀ (y : Y), IsPVMIn (MB y).op) (hR : IsPVMIn R.op) : (registeredReplacementStrategy Ξ G hΞ t₀ MA MB q R hMA hMB hR).value = ((Ξ.reg I).expandA t₀).povmValue G (replaceExtended MA q R) MB

theorem MIPRE.Introspection.registeredReplacementStrategy_value_loss {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ ℬ] [StarProper ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} {I : Type u_9} {T : Type u_10} [Fintype X] [DecidableEq X] [Fintype Y] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] [Fintype I] [DecidableEq I] [Fintype T] [DecidableEq T] [Nonempty I] (G : Game X Y A B) (hΞ : ‖Ξ.ψ‖ = 1) (t₀ : T) (MA : X → POVMIn A (Matrix I I 𝒜)) (MB : Y → POVMIn B (Matrix I I ℬ)) (q : X) (M : POVMIn C (Matrix I I 𝒜)) (R : POVMIn C (Matrix T T (Matrix I I 𝒜))) (f : C → A) (hMA : ∀ (x : X), IsPVMIn (MA x).op) (hMB : ∀ (y : Y), IsPVMIn (MB y).op) (hselected : MA q = POVMIn.map f M) (hM : IsPVMIn M.op) (hR : IsPVMIn R.op) {δ : ℝ} (hd : ∑ c : C, ((Ξ.reg I).expandA t₀).stateSqNorm ((Matrix.diagonal fun (x : T) => M.op c) - R.op c) ≤ δ) : |(Ξ.reg I).povmValue G MA MB - (registeredReplacementStrategy Ξ G hΞ t₀ MA MB q (POVMIn.map f R) hMA hMB ⋯).value| ≤ 2 * √δ

Quantitative value preservation of the actual registered strategy, including its finite-dimensional packaging.