Physics theoremStatement: AI-adaptedProof: AI-adaptedprecheck pass

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 for every declared spin correlation arrangement of the framework

Physical scope

A conditional bound on the CHSH functional of every declared spin correlation arrangement of the framework: for any declared composite preparation of the two spin-half factors and any two unit directions per station the absolute value of the CHSH functional of the arrangement's sign tables is at most 2 sqrt 2, and the bound is attained by the singlet preparation at the directions displayed on this page. The statement is a model theorem under the framework's composite, observable, measurement and spin readings; it asserts no measured value, no apparatus, no detection efficiency and no empirical fact.

Statement

Let $(V \hat{\otimes} V, ρ, a_{0}, a_{1}, b_{0}, b_{1})$ be a declared spin correlation arrangement of the two declared spin-half factors in the sense of Declared spin correlation arrangement of the framework: two spin-half factors, four directions, joint sign tables and local-response models, with a preparation $ρ \in D (V \hat{\otimes} V)$ , unit directions $a_{i}, b_{j} \in R^{3}$ , outcome laws $ν_{i j}^{ρ} (ε, δ)$ and CHSH functional $S (ν^{ρ})$ as in clauses (d) of that definition and (d) of Binary correlation models: setting-indexed tables of two-valued outcome laws, marginals and the CHSH functional. Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) and the Axiom of Choice (The Axiom of Choice), the hypotheses of the cited mathematical suppliers. Then:

(a) $∣ S (ν^{ρ}) ∣ \leq 2 \sqrt{2}$ for every preparation $ρ$ and all unit directions $a_{0}, a_{1}, b_{0}, b_{1}$ ;

(b) the bound is attained: with $Ψ : = \frac{1}{\sqrt{2}} (κ (e_{+} \otimes e_{-}) - κ (e_{-} \otimes e_{+}))$ and the singlet preparation $ρ_{Ψ} = T_{Ψ, Ψ}$ , for the directions $a_{0} = (0, 0, 1)$ , $a_{1} = (1, 0, 0)$ , $b_{0} = (1, 0, 1) / \sqrt{2}$ , $b_{1} = (- 1, 0, 1) / \sqrt{2}$ one has $S (ν^{ρ_{Ψ}}) = - 2 \sqrt{2}$ , so $∣ S (ν^{ρ_{Ψ}}) ∣ = 2 \sqrt{2}$ .

The statement is a conditional theorem about the declared arrangement model; it asserts no measured value and no apparatus realization.

Facts & Assumptions

Given: A declared spin correlation arrangement with preparation $ρ$ and directions $a_{0}, a_{1}, b_{0}, b_{1}$ ; the outcome laws $ν_{i j}^{ρ}$ and their CHSH functional; the Axiom of Countable Choice and the Axiom of Choice.

[F1]

The arrangement's outcome law is $ν_{i j}^{ρ} (ε, δ) = tr (ρ (P_{a_{i}, ε} \otimes P_{b_{j}, δ}))$ with $P_{a, ε} = \frac{1}{2} (I + ε a \cdot σ)$ ; the correlations are $E_{i j} (ν^{ρ}) = \sum_{ε, δ} ε δ ν_{i j}^{ρ} (ε, δ)$ and $S (ν^{ρ}) = E_{00} + E_{01} + E_{10} - E_{11}$ (Declared spin correlation arrangement of the framework: two spin-half factors, four directions, joint sign tables and local-response models clauses (a), (d), Binary correlation models: setting-indexed tables of two-valued outcome laws, marginals and the CHSH functional clause (d)).

[F2]

The Pauli matrix $σ_{a} = \sum_{i} a_{i} σ_{i}$ for unit $a$ is a self-adjoint involution, $σ_{a}^{2} = I$ , and $P_{a, +} - P_{a, -} = σ_{a}$ (Finite spin matrices clause (e), Declared spin correlation arrangement of the framework: two spin-half factors, four directions, joint sign tables and local-response models clause (a)).

[F3]

The completed tensor product $V \hat{\otimes} V$ carries the bounded tensor calculus: $(S \otimes T) (S^{'} \otimes T^{'}) = (S S^{'}) \otimes (T T^{'})$ , $(S \otimes T)^{*} = S^{*} \otimes T^{*}$ , $∥ S \otimes T ∥ \leq ∥ S ∥ ∥ T ∥$ , and the assignment is linear in each argument (Bounded tensor maps: extension, norm estimate, adjoint and commutation clauses (a), (b), (c)).

[F4]

A density operator $ρ$ is self-adjoint, positive and trace class with $tr ρ = 1$ and $∥ ρ ∥_{1} = 1$ (Density operators and scalar spectral probability clause (a), Trace class operator).

[F5]

Trace class is a two-sided Banach operator ideal: for trace-class $T$ and bounded $A, B$ one has $A T B$ trace class with $∥ A T B ∥_{1} \leq ∥ A ∥ ∥ T ∥_{1} ∥ B ∥$ , and $∥ T ∥ \leq ∥ T ∥_{1}$ (Trace class is a two sided Banach operator ideal clauses 1, 2); the trace is linear on the trace class and $∣ tr T ∣ \leq ∥ T ∥_{1}$ (Trace is absolutely convergent and basis independent).

[F6]

For bounded self-adjoint involutions $A_{0}, A_{1}$ on a Hilbert space $H$ and $B_{0}, B_{1}$ on a Hilbert space $K$ , the operator $C : = A_{0} \otimes (B_{0} + B_{1}) + A_{1} \otimes (B_{0} - B_{1})$ on $H \hat{\otimes} K$ is self-adjoint with $∥ C ∥ \leq 2 \sqrt{2}$ ; equivalently, for every unit vector $ψ$ the CHSH combination of the expectations $⟨ (A_{i} \otimes B_{j}) ψ, ψ ⟩$ is at most $2 \sqrt{2}$ in absolute value (Tsirelson bound clauses (a), (b), (c)).

[F7]

Under the Axiom of Countable Choice and the Axiom of Choice, the singlet preparation and displayed directions satisfy $S (ν^{ρ_{Ψ}}) = - 2 \sqrt{2}$ (The singlet arrangement: directional sign tables, CHSH value 2 sqrt 2 and the failure of local-response models at violating settings clause (b)); that supplier states both hypotheses.

Proof

technique · direct; write the CHSH functional as the trace of the preparation against the CHSH operator, apply the operator-norm bound of the finite-dimensional Tsirelson theorem, and bound the trace by the ideal and trace inequalities

Given: The data of the statement and [F1]-[F7].

1.1givenF1F2F3F5algebra

[CHSH functional as an operator trace] Put $C : = σ_{a_{0}} \otimes (σ_{b_{0}} + σ_{b_{1}}) + σ_{a_{1}} \otimes (σ_{b_{0}} - σ_{b_{1}})$ , a bounded operator on $V \hat{\otimes} V$ by [F3]. For each $(i, j)$ , [F2] gives $σ_{a_{i}} \otimes σ_{b_{j}} = (P_{a_{i}, +} - P_{a_{i}, -}) \otimes (P_{b_{j}, +} - P_{b_{j}, -}) = \sum_{ε, δ} ε δ P_{a_{i}, ε} \otimes P_{b_{j}, δ}$ , a finite sum, so by [F1], the linearity of the finite sum and the linearity of the trace [F5], $E_{i j} (ν^{ρ}) = \sum_{ε, δ} ε δ tr (ρ (P_{a_{i}, ε} \otimes P_{b_{j}, δ})) = tr (ρ \sum_{ε, δ} ε δ (P_{a_{i}, ε} \otimes P_{b_{j}, δ})) = tr (ρ (σ_{a_{i}} \otimes σ_{b_{j}}))$ . Summing the four terms with the CHSH signs and using [F3] and the linearity of the trace gives $S (ν^{ρ}) = tr (ρ C)$ .

1.2givenF2F6

[Operator norm bound] By [F2] the matrices $σ_{a_{i}}, σ_{b_{j}}$ are self-adjoint involutions, so [F6] applies and gives $∥ C ∥ \leq 2 \sqrt{2}$ .

2.1step 1.1step 1.2F4F5algebra

[Trace bound] By [F4] $ρ$ is trace class with $∥ ρ ∥_{1} = 1$ , so [F5] makes $ρ C$ trace class with $∥ ρ C ∥_{1} \leq ∥ ρ ∥_{1} ∥ C ∥ = ∥ C ∥$ , and the trace bound of [F5] gives $∣ tr (ρ C) ∣ \leq ∥ ρ C ∥_{1} \leq ∥ C ∥ \leq 2 \sqrt{2}$ . With step 1.1 this is $∣ S (ν^{ρ}) ∣ \leq 2 \sqrt{2}$ , which is (a).

3.1F7step 2.1∎

[Attainment; the Axiom of Choice enters through F7 here] Clause (b) is exactly [F7] for the singlet preparation and the displayed directions, and step 2.1 shows that no value larger than $2 \sqrt{2}$ occurs. The Axiom of Choice is required at this proof step to invoke the attainment result with its stated hypotheses; the operator-norm derivation of (a) uses the Countable Choice hypothesis of its mathematical suppliers.

Remarks

Sharpness within the declared class. The bound cannot be lowered for the declared arrangement model, because the singlet at the displayed directions attains it (clause (b)). This is a statement about the declared binary sign measurements of the arrangement; it is not an optimality statement for other functionals, for more settings, for unsharp measurements or for other systems.
Where the bound is used. The bound is one half of the contrast of this page: the CHSH functional of any representable model is at most $2$ in absolute value (The CHSH bound for every binary correlation model admitting a local-response representation), while the declared arrangement permits $2 \sqrt{2}$ ; the gap is not a numerical coincidence of the singlet but a property of the framework's binary sharp readouts of self-adjoint involutions.

Depends on

Dependency tree · 2 levels

Sources

N. Brunner, D. Cavalcanti, S. Pironio, V. Scarani and S. Wehner, 'Bell nonlocality', Reviews of Modern Physics 86 (2014) 419, Section II.C.1.a, PDF pages 12-13: the Bell operator of a Bell expression, the CHSH operator, the identity S^2 = 4 + [A1,A2][B1,B2], the conclusion ||S|| <= 2 sqrt 2 and the attainment by the singlet
L. J. Landau, 'On the violation of Bell's inequality in quantum theory', Physics Letters A 120 (1987) 54-56, as reported in the review above: the operator derivation of the CHSH quantum bound used here is verified directly from the operator identity in the proof
J. Binney and D. Skinner, The Physics of Quantum Mechanics, Section 6.1.4, printed pages 111-115 (PDF pages 119-123): the singlet correlation -a.b and the contrast with the bound of a setting-independent response model