The doubled model of a finite pair is a finite pair

Theorem A items 3 and 4 and Theorem F of reports/c6b-paper-proofs.md, §4, for the doubled model Doubling.model hM hψ of Co/Doubling/Model.lean, stated on its bipartite model toBipartite (π = id, πA = L, πB = R):

• The players' operators (opsA_model, opsB_model): the first player's operators of the doubled model are the block-diagonal operators u ⊕ v with u the first player's operator of M and v the second's, and the second player's are v ⊕ u.
• A finite pair (isFinitePair, Lemmas 6–9 of the report): the placements are injective; an operator commuting with every R y commutes with 1 ⊕ 0, so is block diagonal, and its blocks commute with the two players' commutants, so it is an L x (and symmetrically); the traces are the averages ½ (τ_𝒜 + τ_ℬ) (VecTrace.diag2, tr_diag2_L, tr_diag2_R).
• Dyadic pairs (isDyadicPair): the doubled model of a dyadic pair is a dyadic pair, its local algebra having the componentwise units (HasDyadicUnits.prod).
• Order agreement (Theorem A.4, Lemma 10): 0 ≤ x ↔ 0 ≤ L x ↔ 0 ≤ R x (L_nonneg_iff, R_nonneg_iff); with the order agreement of M itself (IsFinitePair.nonneg_iff_A, MIPRE/Foundations/FinitePairOrder.lean), the translation Doubling.equiv : 𝒜 × ℬ ≃⋆ₐ Loc M of the report's local algebra 𝒩 = 𝒜 × ℬ preserves and reflects the order (equiv_nonneg_iff, L_equiv_nonneg_iff).
• No abelian projections (Theorem F, Lemma 11; noAbelianProj_iff): the two algebras of the doubled model have no nonzero abelian projection exactly when the two algebras of M have none.

The players' operators

theorem MIPRE.LIDT.Co.Doubling.opsA_model {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) : (model hM hψ).toBipartite.opsA = VecTrace.diag2Set M.opsA M.opsB

The first player's operators of the doubled model are the block-diagonal operators u ⊕ v over the first and the second player's operators of M.

theorem MIPRE.LIDT.Co.Doubling.opsB_model {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) : (model hM hψ).toBipartite.opsB = VecTrace.diag2Set M.opsB M.opsA

The second player's operators of the doubled model are the block-diagonal operators v ⊕ u over the second and the first player's operators of M.

Traces

The traces are stated on the block-diagonal operators VecTrace.diag2Set, which are the players' operators of the doubled model by opsA_model and opsB_model, rather than on (model hM hψ).toBipartite.opsA: instance synthesis on the space (model hM hψ).toBipartite.H, which is Ampl (Fin 2) M.H only after unfolding SymModel.toBipartite, exceeds the synthesis budget, and every functional applied to an operator of that type needs it.

theorem MIPRE.LIDT.Co.Doubling.tr_diag2_L {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) (τ : VecTrace M.opsA) (σ : VecTrace M.opsB) (x : Loc M) : (τ.diag2 σ).tr ((model hM hψ).L x) = 2⁻¹ * (τ.tr ↑x.1 + σ.tr ↑x.2)

The doubled trace of the first algebra is the average (Lemma 9 of the report): with vector traces τ of the first player's operators of M and σ of the second's, τ_D(L x) = ½ (τ(x₁) + σ(x₂)), where τ_D = τ.diag2 σ is a vector trace of the first player's operators of the doubled model (opsA_model).

theorem MIPRE.LIDT.Co.Doubling.tr_diag2_R {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) (τ : VecTrace M.opsA) (σ : VecTrace M.opsB) (x : Loc M) : (σ.diag2 τ).tr ((model hM hψ).R x) = 2⁻¹ * (σ.tr ↑x.2 + τ.tr ↑x.1)

The doubled trace of the second algebra is the average: τ_D(R x) = ½ (σ(x₂) + τ(x₁)), where τ_D = σ.diag2 τ is a vector trace of the second player's operators of the doubled model (opsB_model).

The doubled model is a finite pair

theorem MIPRE.LIDT.Co.Doubling.isFinitePair {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) : (model hM hψ).toBipartite.IsFinitePair

The doubled model of a finite pair is a finite pair (Theorem A.3 of reports/c6b-paper-proofs.md, §4; Lemmas 6–9): the placements are injective, each player's operators are the commutant of the other's, and both carry the averaged vector traces.

Order agreement

theorem MIPRE.LIDT.Co.Doubling.L_nonneg_iff {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) (x : Loc M) : 0 ≤ (model hM hψ).L x ↔ 0 ≤ x

Order agreement in the doubled model, first placement (Theorem A.4): 0 ≤ L x ↔ 0 ≤ x.

theorem MIPRE.LIDT.Co.Doubling.R_nonneg_iff {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) (x : Loc M) : 0 ≤ (model hM hψ).R x ↔ 0 ≤ x

Order agreement in the doubled model, second placement (Theorem A.4): 0 ≤ R x ↔ 0 ≤ x.

The report's local algebra 𝒜 × ℬ

noncomputable def MIPRE.LIDT.Co.Doubling.equivHom {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) : 𝒜 × ℬ →⋆ₐ[ℂ] Loc M

The translation (a, b) ↦ (π (πA a), π (πB b)), as a ⋆-homomorphism.

Equations

• MIPRE.LIDT.Co.Doubling.equivHom hM = (hM.equivA.toStarAlgHom.comp (StarAlgHom.fst ℂ 𝒜 ℬ)).prod (hM.equivB.toStarAlgHom.comp (StarAlgHom.snd ℂ 𝒜 ℬ))

noncomputable def MIPRE.LIDT.Co.Doubling.equivInv {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) : Loc M →⋆ₐ[ℂ] 𝒜 × ℬ

The inverse translation, as a ⋆-homomorphism.

Equations

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

noncomputable def MIPRE.LIDT.Co.Doubling.equiv {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) : 𝒜 × ℬ ≃⋆ₐ[ℂ] Loc M

The translation of the report's local algebra 𝒩 = 𝒜 × ℬ to the doubled model's, (a, b) ↦ (π (πA a), π (πB b)), a ⋆-isomorphism (IsFinitePair.equivA, .equivB).

Equations

• MIPRE.LIDT.Co.Doubling.equiv hM = StarAlgEquiv.ofStarAlgHom (MIPRE.LIDT.Co.Doubling.equivHom hM) (MIPRE.LIDT.Co.Doubling.equivInv hM) ⋯ ⋯

@[simp]

theorem MIPRE.LIDT.Co.Doubling.equiv_apply {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (n : 𝒜 × ℬ) : (equiv hM) n = (hM.equivA n.1, hM.equivB n.2)

The translation of (a, b) is the pair of its operators.

theorem MIPRE.LIDT.Co.Doubling.model_L_equiv {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) (n : 𝒜 × ℬ) : (model hM hψ).L ((equiv hM) n) = OperatorMatrix.diag2 (M.π (M.πA n.1), M.π (M.πB n.2))

The first placement of a translated element: L (a, b) = π (πA a) ⊕ π (πB b).

theorem MIPRE.LIDT.Co.Doubling.model_R_equiv {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) (n : 𝒜 × ℬ) : (model hM hψ).R ((equiv hM) n) = OperatorMatrix.diag2 (M.π (M.πB n.2), M.π (M.πA n.1))

The second placement of a translated element: R (a, b) = π (πB b) ⊕ π (πA a).

theorem MIPRE.LIDT.Co.Doubling.tr_diag2_L_equiv {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) (τ : VecTrace M.opsA) (σ : VecTrace M.opsB) (n : 𝒜 × ℬ) : (τ.diag2 σ).tr ((model hM hψ).L ((equiv hM) n)) = 2⁻¹ * (τ.tr (M.π (M.πA n.1)) + σ.tr (M.π (M.πB n.2)))

The doubled trace of a translated element, in the vocabulary of M: τ_D(L (a, b)) = ½ (τ(π (πA a)) + σ(π (πB b))).

theorem MIPRE.LIDT.Co.Doubling.equiv_nonneg_iff {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (n : 𝒜 × ℬ) : 0 ≤ (equiv hM) n ↔ 0 ≤ n

The translation preserves and reflects the order.

theorem MIPRE.LIDT.Co.Doubling.L_equiv_nonneg_iff {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (n : 𝒜 × ℬ) : 0 ≤ (model hM hψ).L ((equiv hM) n) ↔ 0 ≤ n

Order agreement for the report's local algebra (Theorem A.4): 0 ≤ L (a, b) ↔ 0 ≤ (a, b).

theorem MIPRE.LIDT.Co.Doubling.R_equiv_nonneg_iff {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (n : 𝒜 × ℬ) : 0 ≤ (model hM hψ).R ((equiv hM) n) ↔ 0 ≤ n

Order agreement for the report's local algebra (Theorem A.4): 0 ≤ R (a, b) ↔ 0 ≤ (a, b).

Dyadic pairs

theorem MIPRE.LIDT.Co.Doubling.isDyadicPair {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (h : M.IsDyadicPair) (hψ : ‖M.ψ‖ = 1) : (model ⋯ hψ).toBipartite.IsDyadicPair

The doubled model of a dyadic pair is a dyadic pair: a finite pair, and its local algebra has the componentwise unital dyadic matrix units (HasDyadicUnits.prod).

Abelian projections

theorem MIPRE.LIDT.Co.Doubling.noAbelianProj_iff {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) : NoAbelianProj (model hM hψ).toBipartite.opsA ∧ NoAbelianProj (model hM hψ).toBipartite.opsB ↔ NoAbelianProj M.opsA ∧ NoAbelianProj M.opsB

No abelian projections in the doubled model (Theorem F of reports/c6b-paper-proofs.md, §4; Lemma 11): the two algebras of the doubled model have no nonzero abelian projection exactly when the two algebras of M have none.

theorem MIPRE.LIDT.Co.Doubling.noAbelianProj_opsA_of_isDyadicPair {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (h : M.IsDyadicPair) (hψ : ‖M.ψ‖ = 1) : NoAbelianProj (model ⋯ hψ).toBipartite.opsA

The doubled model of a dyadic pair has no abelian projections, in its first algebra, the one the orthonormalization tier povm_orthogonalization_finitePair is applied to (report §4, Theorem G, step 4).

theorem MIPRE.LIDT.Co.Doubling.noAbelianProj_opsB_of_isDyadicPair {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (h : M.IsDyadicPair) (hψ : ‖M.ψ‖ = 1) : NoAbelianProj (model ⋯ hψ).toBipartite.opsB

The doubled model of a dyadic pair has no abelian projections, in its second algebra.