Documentation

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

source
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₁
Instances For
    source
    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₁)
    source
    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.

    source
    theorem TsirelsonInequality.tsirelson_inequality_aux :
    √2 * √2 ^ 3 = √2 * (2 * (√2)⁻¹ + 4 * ((√2)⁻¹ * 2⁻¹))
    source
    theorem TsirelsonInequality.sqrt_two_inv_mul_self :
    (√2)⁻¹ * (√2)⁻¹ = 2⁻¹
    source
    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!)