# mathlib3documentation

algebra.star.chsh

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

@[nolint]
structure is_CHSH_tuple {R : Type u_1} [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 : = A₀
• A₁_sa : = A₁
• B₀_sa : = B₀
• B₁_sa : = 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} [ R] [ R] (A₀ A₁ B₀ B₁ : R) (T : 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] [ R] [ R] [ R] (A₀ A₁ B₀ B₁ : R) (T : A₁ B₀ B₁) :
A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ 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!)