mathlib documentation

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

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

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 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 #

structure is_CHSH_tuple {R : Type u_1} [monoid R] [star_monoid R] (A₀ A₁ B₀ B₁ : R) :
  • A₀_inv : A₀ ^ 2 = 1
  • A₁_inv : A₁ ^ 2 = 1
  • B₀_inv : B₀ ^ 2 = 1
  • B₁_inv : B₁ ^ 2 = 1
  • A₀_sa : star A₀ = A₀
  • A₁_sa : star A₁ = A₁
  • B₀_sa : star B₀ = B₀
  • B₁_sa : 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 star_monoid R consists of 4 self-adjoint involutions A₀ A₁ B₀ B₁ such that the Aᵢ commute with the Bⱼ.

The physical interpretation is that A₀ and A₁ are a pair of boolean observables which are spacelike separated from another pair B₀ and B₁ of boolean observables.

theorem CHSH_inequality_of_comm {R : Type u} [ordered_comm_ring R] [star_ordered_ring R] [algebra R] [ordered_semimodule R] (A₀ A₁ B₀ B₁ : R) (T : is_CHSH_tuple A₀ A₁ B₀ B₁) :
A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ 2

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.

We next need some lemmas about numerals in modules and algebras. The awkward appearance of both •ℤ and seems unavoidable because later calculations by abel will introduce •ℤ. If anyone sees how to obtain these from general statements, please improve this!

theorem tsirelson_inequality.two_gsmul_half_smul {α : Type u_1} [add_comm_group α] [module α] {X : α} :
2 •ℤ 2⁻¹ X = X
theorem tsirelson_inequality.neg_two_gsmul_half_smul {α : Type u_1} [add_comm_group α] [module α] {X : α} :
(-2) •ℤ 2⁻¹ X = -X
theorem tsirelson_inequality.smul_two {α : Type u_1} [ring α] [algebra α] {x : } :
x 2 = (2 * x) 1
theorem tsirelson_inequality.smul_four {α : Type u_1} [ring α] [algebra α] {x : } :
x 4 = (4 * x) 1

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

theorem tsirelson_inequality {R : Type u} [ordered_ring R] [star_ordered_ring R] [algebra R] [ordered_semimodule R] [star_algebra R] (A₀ A₁ B₀ B₁ : R) (T : is_CHSH_tuple A₀ A₁ B₀ B₁) :
A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ real.sqrt 2 ^ 3 1

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!)