C_qc is closed, and C_qa ⊆ C_qc

The compactness step of the Tsirelson route (planning/tsirelson-campaign.md, §3.3): the set C_qc of commuting-operator correlations is compact, hence closed, in every finite scenario, so C_qa = closure C_q ⊆ C_qc. With the conditional consumer of MIPRE.Foundations.Tsirelson.Conditional, this reduces the negative answer to Tsirelson's problem, C_qa ⊊ C_qc (blueprint cor:tsirelson), to the halting reduction and an upper semidecider for the commuting-operator value (tsirelson_of_upperRE).

The state space in coordinates. A ℂ-linear functional on the game algebra NCPoly (Gen X Y A B) is determined by its values on words, and every function φ : FreeMonoid (Gen X Y A B) → ℂ extends linearly (extend φ, through the monomial basis; extend_single_one, extend_apply_single_one). For a fixed polynomial z, extend φ z is a finite combination of coordinates of φ, so it is continuous in φ for the product topology (continuous_extend_apply). The state space stateSpace X Y A B is the set of φ whose extension is a cone state (MIPRE.Tsirelson.IsConeState: L 1 = 1 and 0 ≤ Re L m for every m in the cone M). Each of these conditions is closed, so the state space is closed (isClosed_stateSpace).

Boundedness. A cone state is bounded by 1 on every word w (IsConeState.norm_map_single_one_le): 1 - w⋆ w ∈ M by telescoping, so for |α| = 1, 2·1 + α w + (α w)⋆ = (1 + α w)⋆ (1 + α w) + (1 - w⋆ w) ∈ M, and L of it is 2 + 2 Re (α L w); the choice α = -conj (L w) / |L w| gives |L w| ≤ 1. So the state space lies in the product of closed unit disks, and it is compact by Tychonoff (isCompact_stateSpace).

The image. The map φ ↦ (x, y, a, b) ↦ Re φ(e_xa f_yb) (correlationOf) is continuous, and it maps the state space onto C_qc (image_correlationOf_stateSpace): this is MIPRE.Tsirelson.mem_Cqc_iff, whose two directions are the GNS strategy of a cone state and the state of a strategy. Hence C_qc is compact (MIPRE.isCompact_Cqc) and closed (MIPRE.isClosed_Cqc).

Main declarations

• Tsirelson.extend, Tsirelson.continuous_extend_apply;
• Tsirelson.IsConeState.norm_map_single_one_le;
• Tsirelson.stateSpace, Tsirelson.isClosed_stateSpace, Tsirelson.isCompact_stateSpace;
• Tsirelson.correlationOf, Tsirelson.image_correlationOf_stateSpace;
• isCompact_Cqc, isClosed_Cqc, Cqa_subset_Cqc, tsirelson_of_upperRE.

Functionals from their values on words

noncomputable def MIPRE.Tsirelson.extend {G : Type u_1} (φ : FreeMonoid G → ℂ) : NCPoly G →ₗ[ℂ] ℂ

The linear extension of word values φ : FreeMonoid G → ℂ to a ℂ-linear functional on NCPoly G: Σ_w c_w w ↦ Σ_w c_w φ w.

Equations

• MIPRE.Tsirelson.extend φ = (MIPRE.NCPoly.basis.constr ℂ) φ

theorem MIPRE.Tsirelson.extend_apply {G : Type u_1} (φ : FreeMonoid G → ℂ) (z : NCPoly G) : (extend φ) z = ∑ w ∈ z.coeff.support, z.coeff w * φ w

The linear extension, as a finite sum over the support of the coefficients.

@[simp]

theorem MIPRE.Tsirelson.extend_single_one {G : Type u_1} (φ : FreeMonoid G → ℂ) (w : FreeMonoid G) : (extend φ) (NCPoly.single w 1) = φ w

The linear extension takes the prescribed value on each word.

theorem MIPRE.Tsirelson.extend_apply_single_one {G : Type u_1} (L : NCPoly G →ₗ[ℂ] ℂ) : (extend fun (w : FreeMonoid G) => L (NCPoly.single w 1)) = L

A linear functional is the linear extension of its values on words.

theorem MIPRE.Tsirelson.continuous_extend_apply {G : Type u_1} (z : NCPoly G) : Continuous fun (φ : FreeMonoid G → ℂ) => (extend φ) z

For a fixed polynomial, the linear extension is continuous in the word values, for the product topology on FreeMonoid G → ℂ.

Cone states are bounded on words

theorem MIPRE.Tsirelson.IsConeState.norm_map_single_one_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} (hL : IsConeState L) (w : FreeMonoid (Gen X Y A B)) : ‖L (NCPoly.single w 1)‖ ≤ 1

A cone state is bounded by 1 on words. With c = L w and α = -conj c / |c|, the element 2·1 + α w + (α w)⋆ lies in the cone (NCPoly.herm_add_const_mem, from 1 - w⋆ w ∈ M), and its value under L is 2 + 2 Re (α c) = 2 - 2 |c|.

The state space in coordinates

def MIPRE.Tsirelson.stateSpace (X : Type u_1) (Y : Type u_2) (A : Type u_3) (B : Type u_4) [Fintype A] [Fintype B] : Set (FreeMonoid (Gen X Y A B) → ℂ)

The state space of the game algebra, in coordinates: the word values φ : FreeMonoid (Gen X Y A B) → ℂ whose linear extension is a cone state.

Equations

• MIPRE.Tsirelson.stateSpace X Y A B = {φ : FreeMonoid (MIPRE.Tsirelson.Gen X Y A B) → ℂ | MIPRE.Tsirelson.IsConeState (MIPRE.Tsirelson.extend φ)}

theorem MIPRE.Tsirelson.mem_stateSpace_iff {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {φ : FreeMonoid (Gen X Y A B) → ℂ} : φ ∈ stateSpace X Y A B ↔ (extend φ) 1 = 1 ∧ ∀ m ∈ cone X Y A B, 0 ≤ ((extend φ) m).re

Membership in the state space, unfolded: normalisation and positivity on the cone.

theorem MIPRE.Tsirelson.isClosed_stateSpace {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] : IsClosed (stateSpace X Y A B)

The state space is closed in the product topology: each defining condition involves finitely many coordinates, continuously.

theorem MIPRE.Tsirelson.stateSpace_subset_pi {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] : stateSpace X Y A B ⊆ Set.univ.pi fun (x : FreeMonoid (Gen X Y A B)) => Metric.closedBall 0 1

The state space lies in the product of closed unit disks.

theorem MIPRE.Tsirelson.isCompact_stateSpace {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] : IsCompact (stateSpace X Y A B)

The state space is compact: a closed subset of a product of closed disks (Tychonoff).

noncomputable def MIPRE.Tsirelson.correlationOf {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (φ : FreeMonoid (Gen X Y A B) → ℂ) : X → Y → A → B → ℝ

The correlation of word values φ: Re φ(e_xa f_yb), read through the linear extension.

Equations

• MIPRE.Tsirelson.correlationOf φ x y a b = ((MIPRE.Tsirelson.extend φ) (MIPRE.Tsirelson.eG x a * MIPRE.Tsirelson.fG y b)).re

theorem MIPRE.Tsirelson.continuous_correlationOf {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} : Continuous correlationOf

The correlation of word values is continuous in them.

theorem MIPRE.Tsirelson.image_correlationOf_stateSpace {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : correlationOf '' stateSpace X Y A B = Cqc X Y A B

C_qc is the image of the state space under φ ↦ Re φ(e_xa f_yb): a cone state gives a commuting-operator strategy by GNS, and a strategy gives a cone state (mem_Cqc_iff).

theorem MIPRE.isCompact_Cqc {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : IsCompact (Cqc X Y A B)

C_qc is compact: it is the continuous image of the compact state space.

theorem MIPRE.isClosed_Cqc {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : IsClosed (Cqc X Y A B)

C_qc is closed.

theorem MIPRE.Cqa_subset_Cqc {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : Cqa X Y A B ⊆ Cqc X Y A B

C_qa ⊆ C_qc: C_q ⊆ C_qc, and C_qc is closed.

theorem MIPRE.tsirelson_of_upperRE (hred : HaltingReductionQuantum) (hU : CommutingUpperRE) : ∃ (nX : ℕ) (nA : ℕ), Cqa (Fin (nX + 1)) (Fin (nX + 1)) (Fin (nA + 1)) (Fin (nA + 1)) ⊂ Cqc (Fin (nX + 1)) (Fin (nX + 1)) (Fin (nA + 1)) (Fin (nA + 1))

Tsirelson's problem, negative answer, given an upper semidecider (blueprint cor:tsirelson): C_qa ⊊ C_qc in some finite scenario, given the halting reduction and an upper semidecider for the commuting-operator value. Closedness of C_qc, the other hypothesis of tsirelson_of_upperRE_of_isClosed, is isClosed_Cqc.