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

• 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][zbMATH06785026]
• [Bell, On the Einstein Podolsky Rosen Paradox][MR3790629]
• [Tsirelson, Quantum generalizations of Bell's inequality][MR577178]

structure IsCHSHTuple {R : Type u_1} [Monoid R] [StarMul R] (A₀ : R) (A₁ : R) (B₀ : R) (B₁ : R) : Prop

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.

• 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₁

theorem IsCHSHTuple.A₀_inv {R : Type u_1} [Monoid R] [StarMul R] {A₀ : R} {A₁ : R} {B₀ : R} {B₁ : R} (self : IsCHSHTuple A₀ A₁ B₀ B₁) : A₀ ^ 2 = 1

theorem IsCHSHTuple.A₁_inv {R : Type u_1} [Monoid R] [StarMul R] {A₀ : R} {A₁ : R} {B₀ : R} {B₁ : R} (self : IsCHSHTuple A₀ A₁ B₀ B₁) : A₁ ^ 2 = 1

theorem IsCHSHTuple.B₀_inv {R : Type u_1} [Monoid R] [StarMul R] {A₀ : R} {A₁ : R} {B₀ : R} {B₁ : R} (self : IsCHSHTuple A₀ A₁ B₀ B₁) : B₀ ^ 2 = 1

theorem IsCHSHTuple.B₁_inv {R : Type u_1} [Monoid R] [StarMul R] {A₀ : R} {A₁ : R} {B₀ : R} {B₁ : R} (self : IsCHSHTuple A₀ A₁ B₀ B₁) : B₁ ^ 2 = 1

theorem IsCHSHTuple.A₀_sa {R : Type u_1} [Monoid R] [StarMul R] {A₀ : R} {A₁ : R} {B₀ : R} {B₁ : R} (self : IsCHSHTuple A₀ A₁ B₀ B₁) : star A₀ = A₀

theorem IsCHSHTuple.A₁_sa {R : Type u_1} [Monoid R] [StarMul R] {A₀ : R} {A₁ : R} {B₀ : R} {B₁ : R} (self : IsCHSHTuple A₀ A₁ B₀ B₁) : star A₁ = A₁

theorem IsCHSHTuple.B₀_sa {R : Type u_1} [Monoid R] [StarMul R] {A₀ : R} {A₁ : R} {B₀ : R} {B₁ : R} (self : IsCHSHTuple A₀ A₁ B₀ B₁) : star B₀ = B₀

theorem IsCHSHTuple.B₁_sa {R : Type u_1} [Monoid R] [StarMul R] {A₀ : R} {A₁ : R} {B₀ : R} {B₁ : R} (self : IsCHSHTuple A₀ A₁ B₀ B₁) : star B₁ = B₁

theorem IsCHSHTuple.A₀B₀_commutes {R : Type u_1} [Monoid R] [StarMul R] {A₀ : R} {A₁ : R} {B₀ : R} {B₁ : R} (self : IsCHSHTuple A₀ A₁ B₀ B₁) : A₀ * B₀ = B₀ * A₀

theorem IsCHSHTuple.A₀B₁_commutes {R : Type u_1} [Monoid R] [StarMul R] {A₀ : R} {A₁ : R} {B₀ : R} {B₁ : R} (self : IsCHSHTuple A₀ A₁ B₀ B₁) : A₀ * B₁ = B₁ * A₀

theorem IsCHSHTuple.A₁B₀_commutes {R : Type u_1} [Monoid R] [StarMul R] {A₀ : R} {A₁ : R} {B₀ : R} {B₁ : R} (self : IsCHSHTuple A₀ A₁ B₀ B₁) : A₁ * B₀ = B₀ * A₁

theorem IsCHSHTuple.A₁B₁_commutes {R : Type u_1} [Monoid R] [StarMul R] {A₀ : R} {A₁ : R} {B₀ : R} {B₁ : R} (self : IsCHSHTuple A₀ A₁ B₀ B₁) : A₁ * B₁ = B₁ * A₁

theorem CHSH_id {R : Type u} [CommRing R] {A₀ : R} {A₁ : R} {B₀ : R} {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} [OrderedCommRing R] [StarRing R] [StarOrderedRing R] [Algebra ℝ R] [OrderedSMul ℝ R] (A₀ : R) (A₁ : R) (B₀ : R) (B₁ : R) (T : IsCHSHTuple 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 TsirelsonInequality.tsirelson_inequality_aux : √2 * √2 ^ 3 = √2 * (2 * (√2)⁻¹ + 4 * ((√2)⁻¹ * 2⁻¹))

theorem TsirelsonInequality.sqrt_two_inv_mul_self : (√2)⁻¹ * (√2)⁻¹ = 2⁻¹

theorem tsirelson_inequality {R : Type u} [OrderedRing R] [StarRing R] [StarOrderedRing R] [Algebra ℝ R] [OrderedSMul ℝ R] [StarModule ℝ R] (A₀ : R) (A₁ : R) (B₀ : R) (B₁ : R) (T : IsCHSHTuple A₀ 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!)