TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Tsirelson bound

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H, K$ be complex Hilbert spaces (Hilbert space) and let $A_{0}, A_{1} \in B (H)$ , $B_{0}, B_{1} \in B (K)$ be bounded self-adjoint operators (A bounded linear operator between normed spaces, Self-adjoint, positive, unitary and normal operators) with $A_{i}^{2} = I_{H}$ and $B_{j}^{2} = I_{K}$ (The Hilbert-space adjoint of a bounded operator). Let $H \hat{\otimes} K$ be the completed tensor product of Hilbert tensor construction: inner product, completion and product bases and put

$C : = A_{0} \otimes (B_{0} + B_{1}) + A_{1} \otimes (B_{0} - B_{1}) \in B (H \hat{\otimes} K) .$

Then:

(a) $C$ is self-adjoint and $C^{2} = 4 I_{H \hat{\otimes} K} - [A_{0}, A_{1}] \otimes [B_{0}, B_{1}];$

(b) $∥ C^{2} ∥ \leq 8$ and $∥ C ∥ \leq 2 \sqrt{2}$ in the operator norm (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Hilbert-adjoint identities);

(c) for all $ψ, ψ^{'} \in H \hat{\otimes} K$ , $∣ ⟨ C ψ, ψ^{'} ⟩ ∣ \leq 2 \sqrt{2} ∥ ψ ∥ ∥ ψ^{'} ∥$ (this is the Tsirelson bound for the stated pair of binary sharp models); consequently the absolute value of the CHSH combination of the four expectations $⟨ (A_{i} \otimes B_{j}) ψ, ψ ⟩$ of a unit vector $ψ$ is at most $2 \sqrt{2}$ ;

(d) the bound is attained on $H = K = C^{2}$ : let $σ_{x}, σ_{y}, σ_{z}$ be the Pauli matrices of Finite spin matrices, let $Ψ : = \frac{1}{\sqrt{2}} (e_{+} \otimes e_{-} - e_{-} \otimes e_{+})$ with the orthonormal basis $(e_{+}, e_{-})$ of $C^{2}$ , put $σ_{a} : = a_{x} σ_{x} + a_{y} σ_{y} + a_{z} σ_{z}$ for a unit vector $a \in R^{3}$ , and take $A_{0} : = σ_{z}$ , $A_{1} : = σ_{x}$ , $B_{0} : = σ_{(z + x) / \sqrt{2}}$ , $B_{1} : = σ_{(z - x) / \sqrt{2}}$ ; then $⟨ σ_{a} \otimes σ_{b} Ψ, Ψ ⟩ = - a \cdot b$ for all unit $a, b$ , and $⟨ C Ψ, Ψ ⟩ = - 2 \sqrt{2}$ , so $∣ ⟨ C Ψ, Ψ ⟩ ∣ = 2 \sqrt{2}$ ;

(e) a comparison with the stated local model: if in addition $A_{0}, A_{1}, B_{0}, B_{1}$ are four $\pm 1$ -valued random variables on one probability space, then the absolute value of their CHSH combination is at most $2$ (The CHSH bound and the finite-sampling law for independent trials (a)); this is a statement about that explicitly specified common-outcome model, not about all theories, and it is not compared here with any reported experiment.

The theorem is a mathematical statement about bounded operators; no measurement, preparation or empirical claim is asserted.

Facts & Assumptions

Given: Countable Choice; complex Hilbert spaces $H, K$ ; self-adjoint involutions $A_{0}, A_{1} \in B (H)$ , $B_{0}, B_{1} \in B (K)$ ; the completed tensor product $H \hat{\otimes} K$ ; the operator $C$ .

[F1]

The completed tensor product is a complex Hilbert space containing the algebraic tensor product densely, and the elementary tensors $u \otimes v$ have inner products $⟨ u \otimes v, u^{'} \otimes v^{'} ⟩ = ⟨ u, u^{'} ⟩ ⟨ v, v^{'} ⟩$ ; $∥ u \otimes v ∥ = ∥ u ∥ ∥ v ∥$ (Hilbert tensor construction: inner product, completion and product bases, Hilbert space).

[F2]

For bounded $S, S^{'} \in B (H)$ , $T, T^{'} \in B (K)$ : $(S \otimes T) (S^{'} \otimes T^{'}) = (S S^{'}) \otimes (T T^{'})$ , $S \otimes I_{K}$ and $I_{H} \otimes T$ commute, $(S \otimes T)^{*} = S^{*} \otimes T^{*}$ , and $∥ S \otimes T ∥ \leq ∥ S ∥ ∥ T ∥$ ; the identity operator on $H \hat{\otimes} K$ is $I_{H} \otimes I_{K}$ (Bounded tensor maps: extension, norm estimate, adjoint and commutation).

[F3]

For bounded operators on Hilbert spaces, the adjoint is additive and conjugate-linear, $(T S)^{*} = S^{*} T^{*}$ , $T^{* *} = T$ , $∥ T^{*} ∥ = ∥ T ∥$ and $∥ T^{*} T ∥ = ∥ T ∥^{2}$ under Countable Choice (Hilbert-adjoint identities). From The operator norm as the least bound and as the unit-sphere or unit-ball supremum, $∥ T S x ∥ \leq ∥ T ∥ ∥ S x ∥ \leq ∥ T ∥ ∥ S ∥ ∥ x ∥$ ; taking the supremum over the unit ball gives $∥ T S ∥ \leq ∥ T ∥ ∥ S ∥$ . Likewise the vector triangle inequality gives $∥ T + S ∥ \leq ∥ T ∥ + ∥ S ∥$ . These estimates include zero spaces.

[F4]

For a bounded operator $T$ and all $ψ, ψ^{'}$ , $∣ ⟨ T ψ, ψ^{'} ⟩ ∣ \leq ∥ T ∥ ∥ ψ ∥ ∥ ψ^{'} ∥$ by Cauchy–Schwarz and the norm definition (Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors, The operator norm as the least bound and as the unit-sphere or unit-ball supremum). A self-adjoint involution satisfies $T^{*} T = T T^{*} = I$ , so it is unitary in the Hilbert-space sense (Self-adjoint, positive, unitary and normal operators).

[F5]

The Pauli matrices are self-adjoint, $σ_{i}^{2} = I_{2}$ , $σ_{x} σ_{y} = i σ_{z}$ and cyclically, and $σ_{a}$ for a unit vector $a$ is self-adjoint with $σ_{a}^{2} = I_{2}$ , because $σ_{a}^{2} = \sum_{i, j} a_{i} a_{j} σ_{i} σ_{j} = \sum_{i} a_{i}^{2} I_{2} + \sum_{i \neq j} a_{i} a_{j} σ_{i} σ_{j} = ∥ a ∥^{2} I_{2}$ by the anticommutation relations $σ_{i} σ_{j} + σ_{j} σ_{i} = 2 δ_{i j} I_{2}$ (Finite spin matrices).

[F6]

If $A_{0}, A_{1}, B_{0}, B_{1} : Ω \to {- 1, 1}$ are random variables on a probability space, then $∣ E [A_{0} B_{0}] + E [A_{0} B_{1}] + E [A_{1} B_{0}] - E [A_{1} B_{1}] ∣ \leq 2$ , with no choice principle used (The CHSH bound and the finite-sampling law for independent trials (a)).

[F7]

A bounded self-adjoint involution satisfies $∥ T x ∥^{2} = ⟨ T x, T x ⟩ = ⟨ x, T^{*} T x ⟩ = ∥ x ∥^{2}$ . Thus $∥ A_{i} ∥, ∥ B_{j} ∥ \leq 1$ (with equality on nonzero factor spaces), and the estimate proved in [F3] gives $∥ A_{0} A_{1} ∥ \leq ∥ A_{0} ∥ ∥ A_{1} ∥ \leq 1$ (The Hilbert-space adjoint of a bounded operator, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

Proof

1.1F1F2F3F7algebra

[Self-adjointness and the square identity] By [F2] and [F3], $(S \otimes T)^{*} = S^{*} \otimes T^{*}$ for the four tensor products entering $C$ , so every summand is self-adjoint and $C^{*} = C$ . Expanding the square with [F2] and [F7] (all operators below are bounded, so products may be reassociated), $C^{2} = (A_{0} \otimes (B_{0} + B_{1}))^{2} + (A_{1} \otimes (B_{0} - B_{1}))^{2} + (A_{0} \otimes (B_{0} + B_{1})) (A_{1} \otimes (B_{0} - B_{1})) + (A_{1} \otimes (B_{0} - B_{1})) (A_{0} \otimes (B_{0} + B_{1}))$ ; using $A_{i}^{2} = I$ and $B_{j}^{2} = I$ together with $(B_{0} + B_{1})^{2} = 2 I + {B_{0}, B_{1}}$ , $(B_{0} - B_{1})^{2} = 2 I - {B_{0}, B_{1}}$ , $(B_{0} + B_{1}) (B_{0} - B_{1}) = [B_{1}, B_{0}]$ and $(B_{0} - B_{1}) (B_{0} + B_{1}) = [B_{0}, B_{1}]$ , the first two summands total $I_{H} \otimes (2 I_{K} + {B_{0}, B_{1}}) + I_{H} \otimes (2 I_{K} - {B_{0}, B_{1}}) = 4 I_{H \hat{\otimes} K}$ , while the cross terms total $- A_{0} A_{1} \otimes [B_{0}, B_{1}] + A_{1} A_{0} \otimes [B_{0}, B_{1}] = - [A_{0}, A_{1}] \otimes [B_{0}, B_{1}]$ ; hence $C^{2} = 4 I - [A_{0}, A_{1}] \otimes [B_{0}, B_{1}]$ .

1.2F1F5algebra

[The singlet correlations] On $C^{2}$ with orthonormal basis $(e_{+}, e_{-})$ define $Ψ : = \frac{1}{\sqrt{2}} (e_{+} \otimes e_{-} - e_{-} \otimes e_{+})$ ; then $∥ Ψ ∥ = 1$ by [F1]. Direct computation with the displayed Pauli matrices gives $σ_{x} e_{+} = e_{-}$ , $σ_{x} e_{-} = e_{+}$ , $σ_{y} e_{+} = i e_{-}$ , $σ_{y} e_{-} = - i e_{+}$ , $σ_{z} e_{+} = e_{+}$ and $σ_{z} e_{-} = - e_{-}$ . Hence $σ_{i} \otimes σ_{i} Ψ = - Ψ$ for $i = x, y, z$ (the two elementary tensors of the difference receive the same sign change), For clarity put $q = (e_{+} \otimes e_{-} + e_{-} \otimes e_{+}) / \sqrt{2}$ and $d_{\pm} = (e_{+} \otimes e_{+} \pm e_{-} \otimes e_{-}) / \sqrt{2}$ . Direct Pauli actions give $(σ_{x} \otimes σ_{y}) Ψ = - i q$ , $(σ_{y} \otimes σ_{x}) Ψ = i q$ , $(σ_{x} \otimes σ_{z}) Ψ = - d_{+}$ , $(σ_{z} \otimes σ_{x}) Ψ = d_{+}$ , $(σ_{y} \otimes σ_{z}) Ψ = i d_{-}$ and $(σ_{z} \otimes σ_{y}) Ψ = - i d_{-}$ . Each of $q, d_{+}, d_{-}$ is orthogonal to $Ψ$ by the elementary product-basis pairings, so every off-diagonal correlation is zero. therefore $⟨ σ_{i} \otimes σ_{j} Ψ, Ψ ⟩ = - δ_{i j}$ , and for unit vectors $a, b$ , $⟨ σ_{a} \otimes σ_{b} Ψ, Ψ ⟩ = \sum_{i, j} a_{i} b_{j} (- δ_{i j}) = - a \cdot b$ , with $σ_{a}, σ_{b}$ self-adjoint involutions by [F5].

2.1step 1.1F2F3F7algebra

[The norm bound] By [F3] and [F7], $∥ [A_{0}, A_{1}] ∥ \leq ∥ A_{0} A_{1} ∥ + ∥ A_{1} A_{0} ∥ \leq 2$ and $∥ [B_{0}, B_{1}] ∥ \leq 2$ , so [F2] gives $∥ [A_{0}, A_{1}] \otimes [B_{0}, B_{1}] ∥ \leq 4$ ; hence $∥ C^{2} ∥ \leq 4 + 4 = 8$ from step 1.1 and the triangle inequality. Since $C$ is self-adjoint by step 1.1, [F3] gives $∥ C ∥^{2} = ∥ C^{*} C ∥ = ∥ C^{2} ∥ \leq 8$ , so $∥ C ∥ \leq 2 \sqrt{2}$ .

2.2step 1.2F5algebra

[Attainment] Take $A_{0} = σ_{z}$ , $A_{1} = σ_{x}$ , $B_{0} = σ_{(z + x) / \sqrt{2}}$ , $B_{1} = σ_{(z - x) / \sqrt{2}}$ , all self-adjoint involutions by [F5]. By step 1.2 the four expectations are $E_{00} = - z \cdot \frac{z + x}{\sqrt{2}} = - \frac{1}{\sqrt{2}}$ , $E_{01} = - z \cdot \frac{z - x}{\sqrt{2}} = - \frac{1}{\sqrt{2}}$ , $E_{10} = - x \cdot \frac{z + x}{\sqrt{2}} = - \frac{1}{\sqrt{2}}$ and $E_{11} = - x \cdot \frac{z - x}{\sqrt{2}} = + \frac{1}{\sqrt{2}}$ , because $x \cdot z = 0$ and $x \cdot x = z \cdot z = 1$ . The CHSH combination of the operator $C$ is $E_{00} + E_{01} + E_{10} - E_{11} = - \frac{4}{\sqrt{2}} = - 2 \sqrt{2}$ , so $∣ ⟨ C Ψ, Ψ ⟩ ∣ = 2 \sqrt{2}$ and the bound (c) is attained.

3.1step 2.1F4algebra

[The quadratic-form bound] For all $ψ, ψ^{'}$ , [F4] and step 2.1 give $∣ ⟨ C ψ, ψ^{'} ⟩ ∣ \leq ∥ C ∥ ∥ ψ ∥ ∥ ψ^{'} ∥ \leq 2 \sqrt{2} ∥ ψ ∥ ∥ ψ^{'} ∥$ ; for a unit vector this is clause (c), and writing $A_{i} \otimes B_{j}$ as self-adjoint operators with the CHSH combination equal to $C$ expresses the four-term combination as $⟨ C ψ, ψ ⟩$ .

4.1F6∎

[Local comparison] Clause (e) is exactly [F6] applied to the four $\pm 1$ -valued random variables of the stated common-outcome model; no relation between that model and the operators of this theorem is asserted.

Depends on

Dependency tree · 2 levels

Sources

N. Brunner, D. Cavalcanti, S. Pironio, V. Scarani, S. Wehner, 'Bell nonlocality', Reviews of Modern Physics 86 (2014) 419, Section II.C.1.a, p. 12, paragraph following equation (31) (CHSH operator bound 2 sqrt 2; the square identity printed there has a plus sign, whereas the minus sign for the displayed CHSH convention is verified locally) and Section II (CHSH inequality (4) and the classical bound S <= 2)
L. J. Landau, 'On the violation of Bell's inequality in quantum theory', Physics Letters A 120 (1987) 54-56 (operator derivation of the CHSH quantum bound), as reported and used in the review above; the operator square identity used here is verified directly in the proof