bell_violation
plain-language theorem explainer
Quantum mechanics violates the Bell inequality by achieving a Tsirelson bound of sqrt(2) that exceeds the classical CHSH bound of 1. Quantum foundations researchers cite this result to quantify the nonlocal correlations permitted by entangled states under ledger consistency. The proof works as a short tactic sequence that unfolds the two bounds and reduces the inequality to a basic fact about square roots via norm_num and linarith.
Claim. The Tsirelson bound on quantum correlations exceeds the classical CHSH bound: $sqrt(2) > 1$.
background
The module addresses QF-006, deriving nonlocality without signaling from ledger consistency. Entangled particles share ledger entries, producing Bell-violating correlations, while local readings leave the distant party's marginal distribution unchanged. This reconciles apparent nonlocality with the prohibition on faster-than-light information transfer. Upstream results supply the ledger factorization structure and the J-cost calibration from the phi-forcing chain that define the numerical bounds.
proof idea
The tactic proof unfolds tsirelsonBound and chshBound. It proves sqrt(2) > 1 by rewriting 1 as sqrt(1), applying the sqrt_lt_sqrt lemma with norm_num on both sides, then concludes with linarith.
why it matters
This theorem supplies the nonlocality half of the ledger model, directly preceding the no_signaling_theorem in the same module. It embeds quantum correlation bounds inside the Recognition Science forcing chain (T5 J-uniqueness through T8 D=3) and the Recognition Composition Law, confirming that Bell violation arises from global ledger consistency without violating local causality. It closes one link in the derivation of quantum features from the single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.