Empirical: Bell-family predictions on the bipartite singlet

Category: 3-Local (CSD-specific empirical-test re-exports of the LF3 singlet kernel; some items here are QM-generic and may be promoted to Cat-2 Framework on demand).

This module names the LF3 singlet-kernel content as empirical predictions with explicit experimental provenance, providing a regression suite that verifies the CSD volume-ratio account reproduces the well-tested QM predictions about Bell-type experiments.

Phase A items (per specs/qm-empirical-tests.md):

• A1: CHSH at Tsirelson bound. ∃ a a' b b' : DetectorSetting, |S(a, a', b, b')| = 2√2 on the singlet, where S = E(a, b) − E(a, b') + E(a', b) + E(a', b').

• A2: Classical bound violated. 2√2 > 2, named as chsh_classical_bound_violated.

• A3 / A4: No-signalling. Alice's marginal is independent of Bob's setting; symmetric for Bob.

• A5: Singlet marginals uniform. P(A = +) = P(B = +) = 1/2.

• A6: Tsirelson upper bound (inner-product / expectation form). Two forms are exported. The algebraic Khalfin-Tsirelson form (chsh_inner_bound) bounds |Re⟨α, β⟩ − Re⟨α, β'⟩ + Re⟨α', β⟩ + Re⟨α', β'⟩| ≤ 2√2 for any four unit vectors α, α', β, β' in a complex inner product space, proved via the parallelogram law + Cauchy-Schwarz on ℝ². The QM-expectation lift (chsh_qm_tsirelson_bound) lifts this to the bipartite-Pauli CHSH expectation |Re⟨ψ, (σ·a ⊗ σ·b)ψ⟩ ± …| ≤ 2√2 for any unit ψ ∈ ℂ² ⊗ ℂ², via the standard Tsirelson construction α(a, ψ) := (σ·a ⊗ I)ψ, β(b, ψ) := (I ⊗ σ·b)ψ. (The operator-form Loewner-order statement via Mathlib's tsirelson_inequality was the original target but is currently blocked on a missing IsOrderedModule ℝ (Matrix n n ℂ) instance upstream; the algebraic + lift route is mathematically equivalent and lands the same expectation bound.)

Experimental provenance

• Bell 1964: Physics 1, 195 (the classical bound).
• Tsirelson 1980: Lett. Math. Phys. 4, 93 (the quantum bound 2√2).
• Aspect, Grangier, Roger 1982: Phys. Rev. Lett. 49, 91 (laboratory verification of Bell-inequality violation).

The Lean theorems below are derived from LF3 correlation_eq_neg_dot, marginal_a_eq_half, marginal_b_eq_half, no_signalling_strong_readout_a/b, which themselves consume only LF3's algebraic core P_st(a, b, s, t) = (1 − st · a·b)/4 (Kernel.lean). The chain to the empirical-frequency side (LF1 SLLN) sits in LF3/Interface.lean's LF3_singlet_frequency_convergence capstones.

Caveat on ontic grounding

These predictions verify CSD-against-QM equivalence on the projective side. Full ontic grounding (Σ as a compact Kähler manifold, μL as the Kähler volume form) is the LF4 §8 obligation. Until then the empirical content is conditional on the CSD ontic axioms supplying the bridge data and the Dirac-concentration preparation. See [[project-structural-debts]] and [[project-lf4-decisions]].

Singlet correlation function

The CHSH inequality is phrased in terms of the correlation E(a, b) := ⟨ψ⁻| σ·a ⊗ σ·b |ψ⁻⟩ = −a·b for the singlet |ψ⁻⟩ (proved inside LF3 as singlet_pauli_correlation for the operator form, and as correlation_eq_neg_dot for the operational pointer-sector form). The latter is the canonical empirical-prediction form: it states the correlation as a finite sum ∑_{s, t} st·P_st(a, b) over the strong-readout pointer-sector probabilities, exactly the quantity an experimentalist measures.

noncomputable def CSD.Empirical.Bell.correlation (a b : LF3.DetectorSetting) : ℝ

Singlet correlation function in operational form: the signed sum ∑_{s, t} st·P_st(a, b) over the joint pointer-sector probabilities in the strong-readout limit, equal to −a·b for the singlet.

This is the experimental quantity directly measured in Bell-type experiments (after Alice and Bob aggregate joint outcomes per setting pair).

Equations

• CSD.Empirical.Bell.correlation a b = ∑ st : CSD.LF3.Sign × CSD.LF3.Sign, st.1.val * st.2.val * CSD.LF3.P_st a b st.1 st.2

theorem CSD.Empirical.Bell.correlation_eq_neg_dot (a b : LF3.DetectorSetting) : correlation a b = -LF3.dotR a b

Closed form: E(a, b) = −a·b for the singlet.

This re-states LF3.correlation_eq_neg_dot as an empirical-prediction named export.

A3 / A4: no-signalling

Both sides' marginals are independent of the other side's setting. Experimentally verified to high precision; structurally guaranteed in QM by the partial-trace marginal identity. In LF3 this comes from the finite Sign-sum identity for P_st, with no appeal to entanglement structure beyond the kernel.

Experimental verification: Aspect 1982 (locality-loophole-free versions: Hensen 2015, Giustina 2015, Shalm 2015).

theorem CSD.Empirical.Bell.no_signalling_alice (a b b' : LF3.DetectorSetting) (s : LF3.Sign) : ∑ t : LF3.Sign, LF3.P_st a b s t = ∑ t : LF3.Sign, LF3.P_st a b' s t

A3: No-signalling, Alice side. Alice's marginal probability is independent of Bob's setting.

theorem CSD.Empirical.Bell.no_signalling_bob (a a' b : LF3.DetectorSetting) (t : LF3.Sign) : ∑ s : LF3.Sign, LF3.P_st a b s t = ∑ s : LF3.Sign, LF3.P_st a' b s t

A4: No-signalling, Bob side. Bob's marginal probability is independent of Alice's setting.

A5: singlet marginals uniform

For the singlet state, each side sees 1/2 / 1/2 outcomes regardless of setting choice. This is the "maximally mixed marginal" property of the singlet; together with no-signalling it is the operational signature of the singlet's symmetry.

theorem CSD.Empirical.Bell.singlet_marginal_alice (a b : LF3.DetectorSetting) (s : LF3.Sign) : ∑ t : LF3.Sign, LF3.P_st a b s t = 1 / 2

A5: Singlet A-side marginal uniform at 1/2.

theorem CSD.Empirical.Bell.singlet_marginal_bob (a b : LF3.DetectorSetting) (t : LF3.Sign) : ∑ s : LF3.Sign, LF3.P_st a b s t = 1 / 2

A5 (Bob side): Singlet B-side marginal uniform at 1/2.

A2: classical Bell bound violation gap

The classical (Bell 1964) bound on the CHSH operator under any local hidden-variable assignment is |S| ≤ 2. The QM prediction |S| = 2√2 (Tsirelson 1980, saturated by the singlet at canonical angles) violates this bound. The named gap is the empirical falsification of local realism.

def CSD.Empirical.Bell.bellClassicalBoundValue : ℝ

The numerical value 2 of the Bell-1964 classical (LHV) CHSH bound. This is a named constant carrying the value 2, not itself a theorem that any local-hidden-variable model satisfies |S| ≤ 2. The LHV inequality is not formalised in this module (it would require modelling a probability space of hidden variables and a factorisable joint distribution).

Now formalised elsewhere (2026-06-03). The LHV |S| ≤ 2 bound is proved in Empirical/QM/Crypto/E91.lean as CSD.Empirical.QM.E91.lhvCHSH_abs_le_two, over a genuine measure-theoretic hidden-variable model (probability space (Λ, μ) with ±1 local responses and factorisable correlations E(a,b) = ∫ A(a,·)B(b,·) dμ). So bellClassicalBoundValue is now backed by a theorem; this constant is retained because the gap theorem chsh_classical_bound_violated states value < 2√2 rather than open-coding the literal.

Equations

• CSD.Empirical.Bell.bellClassicalBoundValue = 2

theorem CSD.Empirical.Bell.chsh_classical_bound_violated : bellClassicalBoundValue < 2 * √2

A2: The Bell-classical-bound value 2 is strictly less than the quantum Tsirelson bound 2√2. The numerical gap is the empirical falsification of local realism realised by the singlet at canonical angles — under the un-formalised premise that any LHV model satisfies |S| ≤ 2 (Bell 1964). The Lean statement is purely numerical (2 < 2√2).

Experimental verification: Aspect, Grangier, Roger 1982, Phys. Rev. Lett. 49, 91 (and many subsequent loophole-free experiments).

A1: CHSH at Tsirelson bound

The CHSH operator S(a, a', b, b') := E(a, b) − E(a, b') + E(a', b) + E(a', b') evaluated on the singlet achieves |S| = 2√2 at the canonical angles a = ẑ̂_x, a' = ẑ̂_y, b = (ẑ̂_x + ẑ̂_y)/√2, b' = (−ẑ̂_x + ẑ̂_y)/√2 (where ẑ̂_x etc. denote unit vectors along the indicated axis of ℝ³).

Tsirelson 1980 proves |S| ≤ 2√2 for any quantum state (the upper bound, A6 below). A1 here establishes saturation: the singlet at canonical angles realises the Tsirelson bound.

We construct the four detector settings explicitly and compute S algebraically against correlation_eq_neg_dot.

noncomputable def CSD.Empirical.Bell.chshOperator (a a' b b' : LF3.DetectorSetting) : ℝ

CHSH operator evaluated on the singlet correlation function.

Equations

• CSD.Empirical.Bell.chshOperator a a' b b' = CSD.Empirical.Bell.correlation a b - CSD.Empirical.Bell.correlation a b' + CSD.Empirical.Bell.correlation a' b + CSD.Empirical.Bell.correlation a' b'

noncomputable def CSD.Empirical.Bell.detector3 (x y z : ℝ) (h_norm : x ^ 2 + y ^ 2 + z ^ 2 = 1) : LF3.DetectorSetting

Helper: construct a DetectorSetting from three real components (x, y, z) with the unit-norm side condition. Uses WithLp.toLp 2 to build the underlying EuclideanSpace ℝ (Fin 3) value from a tuple.

Equations

• CSD.Empirical.Bell.detector3 x y z h_norm = { vec := !₂[x, y, z], unit := ⋯ }

noncomputable def CSD.Empirical.Bell.chshA : LF3.DetectorSetting

The canonical CHSH detector a = (1, 0, 0) along the x-axis.

Equations

• CSD.Empirical.Bell.chshA = CSD.Empirical.Bell.detector3 1 0 0 CSD.Empirical.Bell.chshA._proof_1

noncomputable def CSD.Empirical.Bell.chshA' : LF3.DetectorSetting

The canonical CHSH detector a' = (0, 1, 0) along the y-axis.

Equations

• CSD.Empirical.Bell.chshA' = CSD.Empirical.Bell.detector3 0 1 0 CSD.Empirical.Bell.chshA'._proof_1

theorem CSD.Empirical.Bell.sqrt2_div_two_sq : (√2 / 2) ^ 2 = 1 / 2

Auxiliary: (√2 / 2) ^ 2 = 1 / 2.

noncomputable def CSD.Empirical.Bell.chshB : LF3.DetectorSetting

The canonical CHSH detector b = (√2/2, √2/2, 0) at 45° in the xy-plane.

Equations

• CSD.Empirical.Bell.chshB = CSD.Empirical.Bell.detector3 (√2 / 2) (√2 / 2) 0 CSD.Empirical.Bell.chshB._proof_1

noncomputable def CSD.Empirical.Bell.chshB' : LF3.DetectorSetting

The canonical CHSH detector b' = (−√2/2, √2/2, 0) at 135° in the xy-plane.

Equations

• CSD.Empirical.Bell.chshB' = CSD.Empirical.Bell.detector3 (-(√2 / 2)) (√2 / 2) 0 CSD.Empirical.Bell.chshB'._proof_1

@[simp]

theorem CSD.Empirical.Bell.chshA_vec_ofLp_0 : chshA.vec.ofLp 0 = 1

Component-evaluation lemmas for the canonical detectors. The .ofLp projection exposes the underlying Fin 3 → ℝ representation (which is WithLp.toLp 2 ![...] definitionally).

@[simp]

theorem CSD.Empirical.Bell.chshA_vec_ofLp_1 : chshA.vec.ofLp 1 = 0

@[simp]

theorem CSD.Empirical.Bell.chshA_vec_ofLp_2 : chshA.vec.ofLp 2 = 0

@[simp]

theorem CSD.Empirical.Bell.chshA'_vec_ofLp_0 : chshA'.vec.ofLp 0 = 0

@[simp]

theorem CSD.Empirical.Bell.chshA'_vec_ofLp_1 : chshA'.vec.ofLp 1 = 1

@[simp]

theorem CSD.Empirical.Bell.chshA'_vec_ofLp_2 : chshA'.vec.ofLp 2 = 0

@[simp]

theorem CSD.Empirical.Bell.chshB_vec_ofLp_0 : chshB.vec.ofLp 0 = √2 / 2

@[simp]

theorem CSD.Empirical.Bell.chshB_vec_ofLp_1 : chshB.vec.ofLp 1 = √2 / 2

@[simp]

theorem CSD.Empirical.Bell.chshB_vec_ofLp_2 : chshB.vec.ofLp 2 = 0

@[simp]

theorem CSD.Empirical.Bell.chshB'_vec_ofLp_0 : chshB'.vec.ofLp 0 = -(√2 / 2)

@[simp]

theorem CSD.Empirical.Bell.chshB'_vec_ofLp_1 : chshB'.vec.ofLp 1 = √2 / 2

@[simp]

theorem CSD.Empirical.Bell.chshB'_vec_ofLp_2 : chshB'.vec.ofLp 2 = 0

theorem CSD.Empirical.Bell.sqrt2_mul_sqrt2 : √2 * √2 = 2

√2 · √2 = 2.

theorem CSD.Empirical.Bell.chsh_singlet_at_optimal_angles : chshOperator chshA chshA' chshB chshB' = -(2 * √2)

A1 (named-witness form): the CHSH operator on the singlet at the canonical angles equals −2√2.

theorem CSD.Empirical.Bell.chsh_singlet_tsirelson_bound : ∃ (a : LF3.DetectorSetting) (a' : LF3.DetectorSetting) (b : LF3.DetectorSetting) (b' : LF3.DetectorSetting), |chshOperator a a' b b'| = 2 * √2

A1: CHSH at the Tsirelson bound. There exist detector settings a, a', b, b' for which the singlet CHSH operator saturates the Tsirelson bound |S(a, a', b, b')| = 2√2.

Combined with A2 (bellClassicalBound < 2√2) and A6 (Tsirelson upper bound), this constitutes the LF3-side formal record of the Bell-inequality violation that Aspect 1982 first verified experimentally.

Experimental verification: Aspect, Grangier, Roger 1982, Phys. Rev. Lett. 49, 91; loophole-free verifications including Hensen et al. 2015, Nature 526, 682; Giustina et al. 2015, Phys. Rev. Lett. 115, 250401; Shalm et al. 2015, Phys. Rev. Lett. 115, 250402.

A6: Tsirelson upper bound (Khalfin-Tsirelson algebraic form)

The Tsirelson 1980 inequality says that for any quantum state — pure or mixed, on any Hilbert space — the CHSH observable on a pair of binary commuting observable families has expectation bounded by 2√2.

We deliver the Khalfin-Tsirelson algebraic form: a purely inner-product-space statement that supplies the load-bearing inequality for any QM realisation. For any (complex) inner product space E and four unit vectors α, α', β, β' ∈ E:

|Re⟨α, β⟩ − Re⟨α, β'⟩ + Re⟨α', β⟩ + Re⟨α', β'⟩| ≤ 2√2.

The QM Tsirelson upper bound follows by the standard Tsirelson construction: set α(a) := (σ·a ⊗ I)ψ, β(b) := (I ⊗ σ·b)ψ for unit ψ. Each is a unit vector (uses (σ·a)² = I), and ⟨ψ, (σ·a ⊗ σ·b)ψ⟩ = ⟨α(a), β(b)⟩ (Hermiticity). Applying the algebraic K-T lemma below yields the QM CHSH bound.

The QM-application lift is the chsh_qm_tsirelson_bound theorem below, which discharges the construction by hand via four auxiliary lemmas (sigmaDotLeft_sq, sigmaDotLeft_isHermitian, sigmaDotLeft_mul_sigmaDotRight, and analogous on the right). It does not route through Mathlib's tsirelson_inequality (which is currently blocked on the missing IsOrderedModule ℝ (Matrix n n ℂ) instance).

Why the algebraic form is the load-bearing content. Tsirelson's original 1980 result is, up to relabeling, exactly the algebraic inner-product inequality below: he derives it via the parallelogram law and Cauchy-Schwarz on ℝ². The QM-application step is mechanical once the algebraic core is in place.

Experimental verification: Tsirelson 1980, Lett. Math. Phys. 4, 93 (theoretical); saturated by the singlet at canonical angles (chsh_singlet_at_optimal_angles, A1).

theorem CSD.Empirical.Bell.sum_le_sqrt_two_mul_sqrt_sum_sq {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : x + y ≤ √2 * √(x ^ 2 + y ^ 2)

Auxiliary: x + y ≤ √2 · √(x² + y²) for any non-negative reals x, y. Cauchy-Schwarz on ℝ² applied to (1, 1) and (x, y).

theorem CSD.Empirical.Bell.chsh_inner_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (α α' β β' : E) (hα : ‖α‖ = 1) (hα' : ‖α'‖ = 1) (hβ : ‖β‖ = 1) (hβ' : ‖β'‖ = 1) : |(inner ℂ α β).re - (inner ℂ α β').re + (inner ℂ α' β).re + (inner ℂ α' β').re| ≤ 2 * √2

A6: Khalfin-Tsirelson algebraic CHSH bound in a complex inner product space.

For any four unit vectors α, α', β, β' in a complex inner product space, the CHSH expression in real-inner-product form is bounded by 2√2:

|Re⟨α, β⟩ − Re⟨α, β'⟩ + Re⟨α', β⟩ + Re⟨α', β'⟩| ≤ 2√2.

Proof. Let S := Re⟨α, β − β'⟩ + Re⟨α', β + β'⟩. By the real-part Cauchy-Schwarz inequality:

• Re⟨α, β − β'⟩ ≤ ‖α‖ · ‖β − β'‖ = ‖β − β'‖ (unit α).
• Re⟨α', β + β'⟩ ≤ ‖α'‖ · ‖β + β'‖ = ‖β + β'‖.

So S ≤ ‖β − β'‖ + ‖β + β'‖. By sum_le_sqrt_two_mul_sqrt_sum_sq and the parallelogram identity ‖β − β'‖² + ‖β + β'‖² = 2(‖β‖² + ‖β'‖²) = 4:

‖β − β'‖ + ‖β + β'‖ ≤ √2 · √(‖β − β'‖² + ‖β + β'‖²) = √2 · √4 = 2√2.

The lower bound on S follows by symmetry (negate α, α').

Experimental verification: Tsirelson 1980 (theoretical); saturated by the singlet at canonical angles via the standard Tsirelson construction α(a) := (σ·a ⊗ I)ψ⁻, β(b) := (I ⊗ σ·b)ψ⁻.

A6 QM-application lift: Tsirelson bound on QM expectation

The algebraic chsh_inner_bound lifts to the QM CHSH expectation via the standard Tsirelson construction:

α(a, ψ) := (σ·a ⊗ I) ψ,        β(b, ψ) := (I ⊗ σ·b) ψ

For unit ψ, each of α(a), α(a'), β(b), β(b') is a unit vector (since (σ·a ⊗ I)² = I is a Hermitian involution, which preserves norms). The inner-product identity

⟨α(a, ψ), β(b, ψ)⟩  =  ⟨ψ, (σ·a ⊗ σ·b) ψ⟩

(from Hermiticity of σ·a ⊗ I plus the Kronecker product identity (σ·a ⊗ I) · (I ⊗ σ·b) = σ·a ⊗ σ·b) then turns the QM CHSH expectation into the inner-product form, and chsh_inner_bound gives ≤ 2√2.

theorem CSD.Empirical.Bell.sigmaDotLeft_sq (a : LF3.DetectorSetting) : LF3.sigmaDotLeft a * LF3.sigmaDotLeft a = 1

(σ·a ⊗ I)² = I as a matrix identity. The kernel of the involution property that underlies norm preservation by the Tsirelson Alice-side operator.

theorem CSD.Empirical.Bell.sigmaDotRight_sq (b : LF3.DetectorSetting) : LF3.sigmaDotRight b * LF3.sigmaDotRight b = 1

(I ⊗ σ·b)² = I.

theorem CSD.Empirical.Bell.sigmaDotLeft_isHermitian (a : LF3.DetectorSetting) : (LF3.sigmaDotLeft a).IsHermitian

σ·a ⊗ I is Hermitian.

theorem CSD.Empirical.Bell.sigmaDotRight_isHermitian (b : LF3.DetectorSetting) : (LF3.sigmaDotRight b).IsHermitian

I ⊗ σ·b is Hermitian.

theorem CSD.Empirical.Bell.sigmaDotLeft_mul_sigmaDotRight (a b : LF3.DetectorSetting) : LF3.sigmaDotLeft a * LF3.sigmaDotRight b = LF3.sigmaDotJoint a b

Kronecker product identity: (σ·a ⊗ I) · (I ⊗ σ·b) = σ·a ⊗ σ·b.

noncomputable def CSD.Empirical.Bell.alphaVec (a : LF3.DetectorSetting) (ψ : EuclideanSpace ℂ (Fin 2 × Fin 2)) : EuclideanSpace ℂ (Fin 2 × Fin 2)

The Tsirelson construction vector α(a, ψ) := (σ·a ⊗ I) ψ.

Equations

• CSD.Empirical.Bell.alphaVec a ψ = (Matrix.toEuclideanLin (CSD.LF3.sigmaDotLeft a)) ψ

noncomputable def CSD.Empirical.Bell.betaVec (b : LF3.DetectorSetting) (ψ : EuclideanSpace ℂ (Fin 2 × Fin 2)) : EuclideanSpace ℂ (Fin 2 × Fin 2)

The Tsirelson construction vector β(b, ψ) := (I ⊗ σ·b) ψ.

Equations

• CSD.Empirical.Bell.betaVec b ψ = (Matrix.toEuclideanLin (CSD.LF3.sigmaDotRight b)) ψ

theorem CSD.Empirical.Bell.norm_alphaVec (a : LF3.DetectorSetting) (ψ : EuclideanSpace ℂ (Fin 2 × Fin 2)) : ‖alphaVec a ψ‖ = ‖ψ‖

‖α(a, ψ)‖ = ‖ψ‖: the Alice-side Tsirelson vector preserves the norm of ψ, because σ·a ⊗ I is a Hermitian involution.

theorem CSD.Empirical.Bell.norm_betaVec (b : LF3.DetectorSetting) (ψ : EuclideanSpace ℂ (Fin 2 × Fin 2)) : ‖betaVec b ψ‖ = ‖ψ‖

‖β(b, ψ)‖ = ‖ψ‖.

theorem CSD.Empirical.Bell.inner_alphaVec_betaVec (a b : LF3.DetectorSetting) (ψ : EuclideanSpace ℂ (Fin 2 × Fin 2)) : inner ℂ (alphaVec a ψ) (betaVec b ψ) = inner ℂ ψ ((Matrix.toEuclideanLin (LF3.sigmaDotJoint a b)) ψ)

The inner-product identity at the heart of the Tsirelson construction: ⟨α(a, ψ), β(b, ψ)⟩ = ⟨ψ, (σ·a ⊗ σ·b) ψ⟩.

theorem CSD.Empirical.Bell.chsh_qm_tsirelson_bound (a a' b b' : LF3.DetectorSetting) (ψ : EuclideanSpace ℂ (Fin 2 × Fin 2)) (hψ : ‖ψ‖ = 1) : |(inner ℂ ψ ((Matrix.toEuclideanLin (LF3.sigmaDotJoint a b)) ψ)).re - (inner ℂ ψ ((Matrix.toEuclideanLin (LF3.sigmaDotJoint a b')) ψ)).re + (inner ℂ ψ ((Matrix.toEuclideanLin (LF3.sigmaDotJoint a' b)) ψ)).re + (inner ℂ ψ ((Matrix.toEuclideanLin (LF3.sigmaDotJoint a' b')) ψ)).re| ≤ 2 * √2

A6 QM form: Tsirelson upper bound on bipartite Pauli CHSH expectation. For any unit ψ : EuclideanSpace ℂ (Fin 2 × Fin 2) and any unit detector settings a, a', b, b' : DetectorSetting,

|Re⟨ψ, (σ·a ⊗ σ·b)ψ⟩ − Re⟨ψ, (σ·a ⊗ σ·b')ψ⟩ + Re⟨ψ, (σ·a' ⊗ σ·b)ψ⟩
   + Re⟨ψ, (σ·a' ⊗ σ·b')ψ⟩| ≤ 2√2.

Proved by the standard Tsirelson construction α(a, ψ) := (σ·a ⊗ I)ψ, β(b, ψ) := (I ⊗ σ·b)ψ, followed by the algebraic chsh_inner_bound.

Experimental verification: Tsirelson 1980, Lett. Math. Phys. 4, 93. Saturation by the singlet (ψ = singlet) at canonical angles (chsh_singlet_at_optimal_angles).