ExampleConstruction: AI-adaptedVerification: 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.

Spin singlet CHSH

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $V = C^{2}$ carry the orthonormal basis $(e_{+}, e_{-})$ and let $σ_{x}, σ_{y}, σ_{z}$ be the Pauli matrices of Finite spin matrices (e), with $σ_{a} : = \sum_{i \in {x, y, z}} a_{i} σ_{i}$ for $a \in R^{3}$ ; on the completed tensor product $V \hat{\otimes} V$ use the inner product of Hilbert tensor construction: inner product, completion and product bases. Define the singlet vector $Ψ : = \frac{1}{\sqrt{2}} (e_{+} \otimes e_{-} - e_{-} \otimes e_{+}) \in V \hat{\otimes} V .$ Then:

(a) $∥ Ψ ∥ = 1$ and $⟨ (σ_{i} \otimes σ_{j}) Ψ, Ψ ⟩ = - δ_{i j}$ for all $i, j \in {x, y, z}$ ;

(b) for all unit vectors $a, b \in R^{3}$ the singlet correlation is $⟨ (σ_{a} \otimes σ_{b}) Ψ, Ψ ⟩ = - a \cdot b;$

(c) with the unit vectors $a_{0} : = (1, 0, 0)$ , $a_{1} : = (0, 1, 0)$ , $b_{0} : = (1, 1, 0) / \sqrt{2}$ , $b_{1} : = (1, - 1, 0) / \sqrt{2}$ the CHSH combination of the four correlations $E_{i j} : = ⟨ (σ_{a_{i}} \otimes σ_{b_{j}}) Ψ, Ψ ⟩$ satisfies $E_{00} + E_{01} + E_{10} - E_{11} = - 2 \sqrt{2}, so ∣ E_{00} + E_{01} + E_{10} - E_{11} ∣ = 2 \sqrt{2},$ which is the value of the Tsirelson bound of Tsirelson bound (b),(c); thus the bound is attained at these settings;

(d) since $2 \sqrt{2} > 2$ , the four numbers $E_{i j}$ of (c) cannot be realized as $E [A_{i} B_{j}]$ for four $\pm 1$ -valued random variables $A_{0}, A_{1}, B_{0}, B_{1}$ on one probability space, by the CHSH inequality for that common-outcome model (Tsirelson bound (e)).

All claims are finite-dimensional linear-algebra statements about the indicated matrices and vectors; no preparation, measurement or experimental claim is made.

Facts & Assumptions

Given: the Pauli matrices $σ_{x}, σ_{y}, σ_{z}$ , the basis $(e_{+}, e_{-})$ of $C^{2}$ , the tensor product $V \hat{\otimes} V$ with its inner product, the vector $Ψ$ , and the unit vectors $a_{0}, a_{1}, b_{0}, b_{1}$ .

[F1]

Pauli algebra and its consequences: $σ_{i}^{2} = I_{2}$ , $σ_{x} σ_{y} = i σ_{z}$ , $σ_{y} σ_{z} = i σ_{x}$ , $σ_{z} σ_{x} = i σ_{y}$ (and the reversed products with the opposite sign), $σ_{i} σ_{j} + σ_{j} σ_{i} = 2 δ_{i j} I_{2}$ ; for unit $a$ the matrix $σ_{a}$ is a self-adjoint involution; and the actions on the basis are $σ_{x} e_{+} = e_{-}$ , $σ_{x} e_{-} = e_{+}$ , $σ_{y} e_{+} = i e_{-}$ , $σ_{y} e_{-} = - i e_{+}$ , $σ_{z} e_{+} = e_{+}$ , $σ_{z} e_{-} = - e_{-}$ by the displayed matrices and matrix-vector multiplication (Finite spin matrices (e), Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes).

[F2]

The tensor product: $V \hat{\otimes} V$ is a complex Hilbert space containing the elementary tensors densely, with $⟨ u \otimes v, u^{'} \otimes v^{'} ⟩ = ⟨ u, u^{'} ⟩ ⟨ v, v^{'} ⟩$ ; the four elementary tensors $e_{\pm} \otimes e_{\pm}$ form an orthonormal basis (Hilbert tensor construction: inner product, completion and product bases, Real and complex inner product spaces, with the inner product linear in the first argument, Hilbert space).

[F3]

The operator $S \otimes T$ on $V \hat{\otimes} V$ is determined on elementary tensors by $(S \otimes T) (u \otimes v) = (S u) \otimes (T v)$ ; sums and scalar multiples of such operators act componentwise, so $(σ_{a} \otimes σ_{b}) Ψ = \sum_{i, j} a_{i} b_{j} (σ_{i} \otimes σ_{j}) Ψ$ ; the inner product is linear in the first argument and additive and conjugate-linear in the second (Hilbert tensor construction: inner product, completion and product bases, Linear map between vector spaces over the same field, Real and complex inner product spaces, with the inner product linear in the first argument).

[F4]

The CHSH inequality for the common-outcome model: for $\pm 1$ -valued random variables $A_{0}, A_{1}, B_{0}, B_{1}$ on one probability space, $∣ E [A_{0} B_{0}] + E [A_{0} B_{1}] + E [A_{1} B_{0}] - E [A_{1} B_{1}] ∣ \leq 2$ ; the Tsirelson bound states that the operator $C = A_{0} \otimes (B_{0} + B_{1}) + A_{1} \otimes (B_{0} - B_{1})$ built from self-adjoint involutions satisfies $∣ ⟨ C ψ, ψ ⟩ ∣ \leq 2 \sqrt{2}$ for every unit $ψ$ (Tsirelson bound (b),(c),(e)).

Verification

1.1F1F2F3algebra

[(a), the nine pairings] By [F2], $∥ Ψ ∥^{2} = (∥ e_{+} \otimes e_{-} ∥^{2} + ∥ e_{-} \otimes e_{+} ∥^{2}) / 2 = 1$ . Using [F1] and [F3]: for $i = j = x$ , $(σ_{x} \otimes σ_{x}) Ψ = (e_{-} \otimes e_{+} - e_{+} \otimes e_{-}) / \sqrt{2} = - Ψ$ , so the pairing is $- 1$ ; for $i = j = y$ , $(σ_{y} \otimes σ_{y}) (e_{+} \otimes e_{-}) = (i e_{-}) \otimes (- i e_{+}) = e_{-} \otimes e_{+}$ and $(σ_{y} \otimes σ_{y}) (e_{-} \otimes e_{+}) = (- i e_{+}) \otimes (i e_{-}) = e_{+} \otimes e_{-}$ , so again $(σ_{y} \otimes σ_{y}) Ψ = - Ψ$ ; for $i = j = z$ , $(σ_{z} \otimes σ_{z}) (e_{+} \otimes e_{-}) = e_{+} \otimes (- e_{-}) = - e_{+} \otimes e_{-}$ and $(σ_{z} \otimes σ_{z}) (e_{-} \otimes e_{+}) = (- e_{-}) \otimes e_{+} = - e_{-} \otimes e_{+}$ , so $(σ_{z} \otimes σ_{z}) Ψ = - Ψ$ . 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}$ .

2.1step 1.1F3F4algebra

[(b) and (c)] By [F3], $(σ_{a} \otimes σ_{b}) Ψ = \sum_{i, j} a_{i} b_{j} (σ_{i} \otimes σ_{j}) Ψ$ , so step 1.1 and the linearity and conjugate-linearity of the inner product give $⟨ (σ_{a} \otimes σ_{b}) Ψ, Ψ ⟩ = \sum_{i, j} a_{i} b_{j} (- δ_{i j}) = - a \cdot b$ , using real $a, b$ . With the four unit vectors displayed in (c) the dot products are $a_{0} \cdot b_{0} = a_{0} \cdot b_{1} = a_{1} \cdot b_{0} = 1 / \sqrt{2}$ and $a_{1} \cdot b_{1} = - 1 / \sqrt{2}$ , so $E_{00} = E_{01} = E_{10} = - 1 / \sqrt{2}$ and $E_{11} = + 1 / \sqrt{2}$ , giving $E_{00} + E_{01} + E_{10} - E_{11} = - 4 / \sqrt{2} = - 2 \sqrt{2}$ ; the bound in [F4] forces $2 \sqrt{2}$ to be the largest possible value of this combination, so the bound is attained.

3.1step 2.1F4algebra∎

[(d)] By [F4], any four $\pm 1$ -valued random variables on one probability space satisfy the CHSH bound 2 for the same combination; since the combination computed in step 2.1 has absolute value $2 \sqrt{2} > 2$ , no such common-outcome model reproduces the four numbers $E_{i j}$ .

Spin singlet CHSH

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources