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
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
(in particular a von Neumann algebra) this is a strict generalization of the usual statement.
R be a
A CHSH tuple in
R consists of
- four elements
A₀ A₁ B₀ B₁ : R, such that
Bⱼis a self-adjoint involution, and
Aᵢcommute with the
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
(and hence commute).
The CHSH inequality says that when
R is an ordered
(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
the order structure is completely determined by the
0 ≤ A iff there exists some
A = star B * B.
There's a nice proof of both bounds in this setting at
The proof given here is purely algebraic.
Future work #
One can show that Tsirelson's inequality is tight.
*-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.
- A₀_inv : A₀ ^ 2 = 1
- A₁_inv : A₁ ^ 2 = 1
- B₀_inv : B₀ ^ 2 = 1
- B₁_inv : B₁ ^ 2 = 1
- A₀_sa : has_star.star A₀ = A₀
- A₁_sa : has_star.star A₁ = A₁
- B₀_sa : has_star.star B₀ = B₀
- B₁_sa : has_star.star B₁ = B₁
- A₀B₀_commutes : A₀ * B₀ = B₀ * A₀
- A₀B₁_commutes : A₀ * B₁ = B₁ * A₀
- A₁B₀_commutes : A₁ * B₀ = B₀ * A₁
- A₁B₁_commutes : A₁ * B₁ = B₁ * A₁
A CHSH tuple in a *-monoid consists of 4 self-adjoint involutions
A₀ A₁ B₀ B₁ such that
Aᵢ commute with the
The physical interpretation is that
A₁ are a pair of boolean observables which
are spacelike separated from another pair
B₁ of boolean observables.
Given a CHSH tuple (A₀, A₁, B₀, B₁) in a commutative ordered
*-algebra over ℝ,
A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2.
(We could work over ℤ[⅟2] if we wanted to!)
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.
In a noncommutative ordered
*-algebra over ℝ,
Tsirelson's bound for a CHSH tuple (A₀, A₁, B₀, B₁) is
A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2^(3/2) • 1.
We prove this by providing an explicit sum-of-squares decomposition of the difference.
(We could work over
ℤ[2^(1/2), 2^(-1/2)] if we really wanted to!)