mathlib documentation

algebra.star.chsh

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

@[nolint]
structure is_CHSH_tuple {R : Type u_1} [monoid R] [star_semigroup R] (A₀ A₁ B₀ B₁ : R) :
Type
  • 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 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.

Instances for is_CHSH_tuple
  • is_CHSH_tuple.has_sizeof_inst
theorem CHSH_id {R : Type u} [comm_ring 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) :
(2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) = 4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁)
theorem CHSH_inequality_of_comm {R : Type u} [ordered_comm_ring R] [star_ordered_ring R] [algebra R] [ordered_smul 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.

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_smul R] [star_module 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!)