Quantum Bell Inequality

The Bell inequality

The Bell inequality is a statistical test that tells apart two kinds of physical theories. In 1964, John Bell showed that any theory using local hidden variables, meaning any account where each particle carries a pre-existing instruction set and no influence travels faster than light, must obey a strict bound on certain correlations. Quantum mechanics, however, predicts that entangled particles can violate this bound. The most common form, the CHSH inequality, states that a particular combination of correlations, written S, must satisfy |S| ≤ 2 for any local hidden variable theory. Quantum mechanics allows values up to 2√2, about 2.83, a limit known as the Tsirelson bound. Experiments, starting with Alain Aspect's 1982 test, have confirmed the quantum prediction.

The history is one of tightening experimental control. Aspect's early experiment measured S = 2.70 ± 0.05, a clear violation. Later experiments closed the loopholes that might have allowed a classical explanation. The module records a modern loophole-free result of S = 2.42 ± 0.02, and notes that local hidden variables have been ruled out at more than 100σ. The statistical power is overwhelming: the quantum description survives every test.

In Recognition Science, the framework models this situation with a concrete picture. The core idea is that entanglement is a shared ledger, a discrete record of events that two particles created together both refer to. Measuring one particle reads that shared entry, and because both particles point to the same record, the correlation is immediate. The framework proves the quantum side of the story: the perfect anticorrelation of a singlet state, the bound on any single correlation, and the Tsirelson bound itself as the maximum possible violation. These are formal theorems in its machine-checked library of formal theorems.

The framework's contribution is not a new experiment but a new explanation of why the bound is what it is. The shared ledger produces correlations that no local hidden variable theory can match, while the ledger structure itself forbids faster-than-light signaling. The module states plainly what is ruled out: local hidden variables, FTL signaling, and any violation of the Tsirelson bound. What remains is the quantum prediction, now derived from a bookkeeping picture rather than assumed as a postulate.

/-- **THEOREM (Quantum Violation)**: With optimal angles, |S| = 2√2.
    This violates the classical bound of 2.

    Calculation:
    E(0, π/4) = -cos(-π/4) = -√2/2
    E(0, 3π/4) = -cos(-3π/4) = √2/2
    E(π/2, π/4) = -cos(π/4) = -√2/2
    E(π/2, 3π/4) = -cos(-π/4) = -√2/2
    S = E(0,π/4) - E(0,3π/4) + E(π/2,π/4) + E(π/2,3π/4)
      = -√2/2 - √2/2 - √2/2 - √2/2 = -2√2
    |S| = 2√2 -/
theorem quantum_violation :
    |optimalCHSH| = tsirelsonBound := by
  rw [optimal_chsh_value, abs_neg, abs_of_pos]
  exact mul_pos (by norm_num : (2 : ℝ) > 0) (Real.sqrt_pos.mpr (by norm_num))

/-- **THEOREM**: Perfect anticorrelation when measuring same direction. -/
theorem perfect_anticorrelation (a : MeasurementAngle) :
    quantumCorrelation a a = -1 := by
  unfold quantumCorrelation
  simp

/-- **THEOREM**: Quantum correlation is bounded by 1. -/
theorem quantum_correlation_bounded (a b : MeasurementAngle) :
    |quantumCorrelation a b| ≤ 1 := by
  unfold quantumCorrelation
  simp only [abs_neg]
  exact abs_cos_le_one _

What this page does not claim

The framework does not prove that the shared ledger is the only possible explanation of Bell violation. The framework does not derive the experimental values from first principles. The framework does not claim to rule out all possible classical explanations beyond local hidden variables.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Quantum/BellInequality.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: