← Back to dashboard

CHSH: the inequality a quantum state can break

Alice and Bob each pick one of two measurement angles on a shared entangled pair. Every pair of choices gives a correlation. Add three, subtract the fourth — that number is S. No local hidden-variable theory can push |S| past 2. Quantum mechanics, measured on the singlet state, reaches 2√2 ≈ 2.828 — Tsirelson’s ceiling. Drag the sliders below to feel it.

Model

Angles

optimal
optimal
optimal
optimal

S

2.828
quantum, at Tsirelson bound
classical: |S| ≤ 2 Tsirelson: |S| ≤ 2√2

Correlation table

b₀b₁
a₀
a₁
S = |⟨a₀ b₀⟩ + ⟨a₀ b₁⟩ + ⟨a₁ b₀⟩ − ⟨a₁ b₁⟩|

What is this?

In PhysProof, all three bounds live in PhysProof/Physics/Quantum/BellTheorem.lean — sorry-free, typechecked by the Lean kernel. The classical ceiling is chsh_inequality; the quantum violation at the angles above is quantum_violates_chsh; Tsirelson’s ceiling is tsirelson_bound. Every loophole-free experiment since Hensen 2015 measures S > 2. That rules out any local hidden-variable account of quantum correlations — including, crucially, any reading of Wheeler’s “It from Bit” in which the “bit” is a pre-existing classical label. The bit is a measurement outcome, not a hidden tag.

Pure client-side computation from closed-form expressions — no simulation, no RNG except when you press randomize. The quantum correlation $-\cos(\theta_a - \theta_b)$ and the triangle-wave LHV $-1 + (2/\pi)\,|\theta_a - \theta_b|$ are the only formulas used.