The Clauser-Horne-Shimony-Holt inequality and Tsirelson's inequality. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We establish a version of the Clauser-Horne-Shimony-Holt (CHSH) inequality (which is a generalization of Bell's inequality). This is a foundational result which implies that quantum mechanics is not a local hidden variable theory.

As usually stated the CHSH inequality requires substantial language from physics and probability, but it is possible to give a statement that is purely about ordered *-algebras. We do that here, to avoid as many practical and logical dependencies as possible. Since the algebra of observables of any quantum system is an ordered *-algebra (in particular a von Neumann algebra) this is a strict generalization of the usual statement.

Let R be a *-ring.

A CHSH tuple in R consists of

• four elements A₀ A₁ B₀ B₁ : R, such that
• each Aᵢ and Bⱼ is a self-adjoint involution, and
• the Aᵢ commute with the Bⱼ.

The physical interpretation is that the four elements are observables (hence self-adjoint) that take values ±1 (hence involutions), and that the Aᵢ are spacelike separated from the Bⱼ (and hence commute).

The CHSH inequality says that when R is an ordered *-ring (that is, a *-ring which is ordered, and for every r : R, 0 ≤ star r * r), which is moreover commutative, we have A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2

On the other hand, Tsirelson's inequality says that for any ordered *-ring we have A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2√2

(A caveat: in the commutative case we need 2⁻¹ in the ring, and in the noncommutative case we need √2 and √2⁻¹. To keep things simple we just assume our rings are ℝ-algebras.)

The proofs I've seen in the literature either assume a significant framework for quantum mechanics, or assume the ring is a C^*-algebra. In the C^*-algebra case, the order structure is completely determined by the *-algebra structure: 0 ≤ A iff there exists some B so A = star B * B. There's a nice proof of both bounds in this setting at https://en.wikipedia.org/wiki/Tsirelson%27s_bound The proof given here is purely algebraic.

Future work #

One can show that Tsirelson's inequality is tight. In the *-ring of n-by-n complex matrices, if A ≤ λ I for some λ : ℝ, then every eigenvalue has absolute value at most λ. There is a CHSH tuple in 4-by-4 matrices such that A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ has 2√2 as an eigenvalue.

References #

• Clauser, Horne, Shimony, Holt, Proposed experiment to test local hidden-variable theories
• Bell, On the Einstein Podolsky Rosen Paradox
• Tsirelson, Quantum generalizations of Bell's inequality

We now prove some rather specialized lemmas in preparation for the Tsirelson inequality, which we hide in a namespace as they are unlikely to be useful elsewhere.

Before proving Tsirelson's bound, we prepare some easy lemmas about √2.