The EPR register in a bipartite model

Introspection's soundness analysis runs on a state |EPR_I⟩ ⊗ |ξ⟩: a maximally entangled register I, shared by the two players, next to whatever else they hold. In the tensor-product model ξ is a vector of ℂ^{H} ⊗ ℂ^{K} and the players' operators are matrices on ℂ^{I} ⊗ ℂ^{H} and ℂ^{I} ⊗ ℂ^{K} (MIPRE.Introspection.registerState). Phase 4 of planning/mipco-track.md keeps the register and abstracts the rest: ξ becomes a bipartite model N, and the state |EPR_I⟩ ⊗ |ξ⟩ its extension by the register (BipartiteModel.reg, the ancilla extension of MIPRE/Foundations/AncillaModel.lean in the vector registerEPR I). The first player's operators are then the I × I matrices over the first player's algebra of N, the second's over the second's; a matrix P on the register acting as P ⊗ 1 is smulKron 1 P.

• The mirror identity (reg_mirror, reg_mirror_smulKron): an operator P on the first player's register acts on the state as its transpose on the second player's. This is the switching trick of the analysis, and it is exact in any model, the register being a matrix factor.
• The register is carried along bijections (regRelabel), split into two registers (regSplit), and extended by one on which nothing acts (regExtend), each by a local isometry carrying the state exactly (MIPRE/Foundations/AncillaIsometry.lean); and the players are exchanged (regSwap).

noncomputable def MIPRE.Introspection.registerEPR (I : Type u_4) [Fintype I] [DecidableEq I] : I × I → ℂ

The maximally entangled state, indexed by an arbitrary finite basis.

Equations

• MIPRE.Introspection.registerEPR I p = if p.1 = p.2 then ↑(√↑(Fintype.card I))⁻¹ else 0

theorem MIPRE.Introspection.registerEPR_eq_weyl {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] : registerEPR (ι → F) = Weyl.epr

The finite-basis EPR definition agrees literally with the Weyl-register definition.

theorem MIPRE.Introspection.registerEPR_equiv {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ≃ J) : registerEPR J ∘ ⇑(e.prodCongr e) = registerEPR I

Simultaneous relabelling of both EPR halves leaves the state unchanged.

theorem MIPRE.Introspection.registerEPR_prod {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] : registerEPR (I × J) = expVec (registerEPR I) (registerEPR J)

EPR on a product basis factors exactly into the two EPR states.

theorem MIPRE.Introspection.registerEPR_norm {I : Type u_1} [Fintype I] [DecidableEq I] [Nonempty I] : ‖evec (registerEPR I)‖ = 1

Unit normalization for a nonempty finite EPR basis.

theorem MIPRE.Introspection.registerEPR_swap {I : Type u_1} [Fintype I] [DecidableEq I] (p : I × I) : registerEPR I p.swap = registerEPR I p

The EPR state is symmetric under the exchange of its halves.

theorem MIPRE.Introspection.kron_one_mulVec_registerEPR {I : Type u_1} [Fintype I] [DecidableEq I] (P : Matrix I I ℂ) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P 1).mulVec (registerEPR I) = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 P.transpose).mulVec (registerEPR I)

The mirror identity of the EPR state: an operator on the first half acts on the state as its transpose on the second half.

Splitting a register of block matrices

def MIPRE.Introspection.regSplitHom {I : Type u_1} {J : Type u_2} {R : Type u_3} [Fintype I] [Fintype J] [Fintype R] {A : Type u_4} [Ring A] [StarRing A] [Algebra ℂ A] (e : I ≃ J × R) : Matrix J J (Matrix R R A) →⋆ₙₐ[ℂ] Matrix I I A

The reindexing of block matrices along e : I ≃ J × R: a block matrix over J of block matrices over R, read as a block matrix over I. It is the players' homomorphism of the register splitting BipartiteModel.regSplit, and depends on nothing else.

Equations

• MIPRE.Introspection.regSplitHom e = (MIPRE.submatrixHom e).comp MIPRE.compHom

def MIPRE.Introspection.regSplitInvHom {I : Type u_1} {J : Type u_2} {R : Type u_3} [Fintype I] [Fintype J] [Fintype R] {A : Type u_4} [Ring A] [StarRing A] [Algebra ℂ A] (e : I ≃ J × R) : Matrix I I A →⋆ₙₐ[ℂ] Matrix J J (Matrix R R A)

Its inverse: a block matrix over I as a block matrix over J of block matrices over R.

Equations

• MIPRE.Introspection.regSplitInvHom e = MIPRE.uncompHom.comp (MIPRE.submatrixHom e.symm)

theorem MIPRE.Introspection.regSplitHom_apply {I : Type u_1} {J : Type u_2} {R : Type u_3} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] {A : Type u_4} [Ring A] [StarRing A] [Algebra ℂ A] (e : I ≃ J × R) (X : Matrix J J (Matrix R R A)) (i i' : I) : (regSplitHom e) X i i' = X (e i).1 (e i').1 (e i).2 (e i').2

theorem MIPRE.Introspection.regSplitInvHom_apply {I : Type u_1} {J : Type u_2} {R : Type u_3} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] {A : Type u_4} [Ring A] [StarRing A] [Algebra ℂ A] (e : I ≃ J × R) (X : Matrix I I A) (j j' : J) (r r' : R) : (regSplitInvHom e) X j j' r r' = X (e.symm (j, r)) (e.symm (j', r'))

@[simp]

theorem MIPRE.Introspection.regSplitHom_inv {I : Type u_1} {J : Type u_2} {R : Type u_3} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] {A : Type u_4} [Ring A] [StarRing A] [Algebra ℂ A] (e : I ≃ J × R) (X : Matrix I I A) : (regSplitHom e) ((regSplitInvHom e) X) = X

@[simp]

theorem MIPRE.Introspection.regSplitInvHom_hom {I : Type u_1} {J : Type u_2} {R : Type u_3} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] {A : Type u_4} [Ring A] [StarRing A] [Algebra ℂ A] (e : I ≃ J × R) (X : Matrix J J (Matrix R R A)) : (regSplitInvHom e) ((regSplitHom e) X) = X

theorem MIPRE.Introspection.regSplitHom_one {I : Type u_1} {J : Type u_2} {R : Type u_3} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] {A : Type u_4} [Ring A] [StarRing A] [Algebra ℂ A] (e : I ≃ J × R) : (regSplitHom e) 1 = 1

theorem MIPRE.Introspection.regSplitInvHom_one {I : Type u_1} {J : Type u_2} {R : Type u_3} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] {A : Type u_4} [Ring A] [StarRing A] [Algebra ℂ A] (e : I ≃ J × R) : (regSplitInvHom e) 1 = 1

def MIPRE.Introspection.regExtendHom {I : Type u_1} {J : Type u_2} {R : Type u_3} [Fintype I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] {A : Type u_4} [Ring A] [StarRing A] [Algebra ℂ A] (e : I ≃ J × R) : Matrix J J A →⋆ₙₐ[ℂ] Matrix I I A

Extending a register of block matrices along e : I ≃ J × R by a register R on which nothing acts: X ↦ X ⊗ 1_R, read along e. It is the players' homomorphism of the register extension BipartiteModel.regExtend, and depends on nothing else.

Equations

• MIPRE.Introspection.regExtendHom e = (MIPRE.submatrixHom (e.trans (Equiv.prodComm J R))).comp (MIPRE.compHom.comp MIPRE.diagHom)

theorem MIPRE.Introspection.regExtendHom_one {I : Type u_1} {J : Type u_2} {R : Type u_3} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] {A : Type u_4} [Ring A] [StarRing A] [Algebra ℂ A] (e : I ≃ J × R) : (regExtendHom e) 1 = 1

@[reducible, inline]

noncomputable abbrev MIPRE.BipartiteModel.reg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) (I : Type u_7) [Fintype I] [DecidableEq I] : BipartiteModel (Matrix (I × I) (I × I) 𝒞) (Matrix I I 𝒜) (Matrix I I ℬ)

The register model: N with an EPR register I adjoined for the two players, in the state |EPR_I⟩ ⊗ ψ. The first player's operators are the I × I matrices over the first player's algebra of N, the second's over the second's.

Equations

• N.reg I = N.expand (MIPRE.Introspection.registerEPR I)

theorem MIPRE.BipartiteModel.norm_reg_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} [Fintype I] [DecidableEq I] [Nonempty I] : ‖(N.reg I).ψ‖ = ‖N.ψ‖

The state of the register model has the norm of the state of N.

theorem MIPRE.BipartiteModel.reg_mirror_smulKron {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} [Fintype I] [DecidableEq I] (X : 𝒜) (P : Matrix I I ℂ) : ((N.reg I).π ((N.reg I).πA (smulKron X P))) (N.reg I).ψ = ((N.reg I).π ((N.reg I).πA (smulKron X 1) * (N.reg I).πB (smulKron 1 P.transpose))) (N.reg I).ψ

The mirror identity in the register model: the first player's register operator X ⊗ P acts on the state as X ⊗ 1 for the first player times 1 ⊗ Pᵀ for the second.

theorem MIPRE.BipartiteModel.reg_mirror {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} [Fintype I] [DecidableEq I] (P : Matrix I I ℂ) : ((N.reg I).π ((N.reg I).πA (smulKron 1 P))) (N.reg I).ψ = ((N.reg I).π ((N.reg I).πB (smulKron 1 P.transpose))) (N.reg I).ψ

The mirror identity: a matrix P on the first player's register acts on the state as its transpose on the second player's.

Moving the register

noncomputable def MIPRE.BipartiteModel.regRelabel {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {J : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (f : I ≃ J) : (N.reg J).LocalIsometry (N.reg I)

Relabelling the register along a bijection f : I ≃ J: the register model on J into the register model on I, the players' operators relabelled by f.

Equations

• N.regRelabel f = N.relabel (MIPRE.Introspection.registerEPR J) (MIPRE.Introspection.registerEPR I) f f

theorem MIPRE.BipartiteModel.regRelabel_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {J : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (f : I ≃ J) : (N.regRelabel f).W (N.reg J).ψ = (N.reg I).ψ

@[simp]

theorem MIPRE.BipartiteModel.regRelabel_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {J : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (f : I ≃ J) (X : Matrix J J 𝒜) : (N.regRelabel f).ΦA X = X.submatrix ⇑f ⇑f

@[simp]

theorem MIPRE.BipartiteModel.regRelabel_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {J : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (f : I ≃ J) (Y : Matrix J J ℬ) : (N.regRelabel f).ΦB Y = Y.submatrix ⇑f ⇑f

noncomputable def MIPRE.BipartiteModel.regSplit {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {J : Type u_5} {R : Type u_6} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] (e : I ≃ J × R) : ((N.reg R).reg J).LocalIsometry (N.reg I)

Splitting the register along e : I ≃ J × R: the register model on J over the register model on R into the register model on I, the players' block matrices of block matrices read as block matrices along e.

Equations

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

theorem MIPRE.BipartiteModel.regSplit_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {J : Type u_5} {R : Type u_6} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] (e : I ≃ J × R) : (N.regSplit e).W ((N.reg R).reg J).ψ = (N.reg I).ψ

theorem MIPRE.BipartiteModel.regSplit_ΦA_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {J : Type u_5} {R : Type u_6} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] (e : I ≃ J × R) : (N.regSplit e).ΦA = Introspection.regSplitHom e

noncomputable def MIPRE.BipartiteModel.regExtend {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {J : Type u_5} {R : Type u_6} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] [Nonempty R] (e : I ≃ J × R) : (N.reg J).LocalIsometry (N.reg I)

Extending the register along e : I ≃ J × R by a register R on which nothing acts: the register model on J into the register model on I, an operator X on J becoming X ⊗ 1_R read along e.

Equations

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

theorem MIPRE.BipartiteModel.regExtend_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {J : Type u_5} {R : Type u_6} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] [Nonempty R] (e : I ≃ J × R) : (N.regExtend e).W (N.reg J).ψ = (N.reg I).ψ

theorem MIPRE.BipartiteModel.regExtend_ΦA_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {J : Type u_5} {R : Type u_6} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] [Nonempty R] (e : I ≃ J × R) : (N.regExtend e).ΦA = Introspection.regExtendHom e

noncomputable def MIPRE.BipartiteModel.regSwap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} [Fintype I] [DecidableEq I] : (N.reg I).swap.LocalIsometry (N.swap.reg I)

Exchanging the players of the register model.

Equations

• N.regSwap = N.swapExpand (MIPRE.Introspection.registerEPR I) (MIPRE.Introspection.registerEPR I)

theorem MIPRE.BipartiteModel.regSwap_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} [Fintype I] [DecidableEq I] : N.regSwap.W (N.reg I).swap.ψ = (N.swap.reg I).ψ

@[simp]

theorem MIPRE.BipartiteModel.regSwap_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} [Fintype I] [DecidableEq I] (Y : Matrix I I ℬ) : N.regSwap.ΦA Y = Y

@[simp]

theorem MIPRE.BipartiteModel.regSwap_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} [Fintype I] [DecidableEq I] (X : Matrix I I 𝒜) : N.regSwap.ΦB X = X