tsirelsonBound
plain-language theorem explainer
The Tsirelson bound supplies the numerical ceiling 2√2 on the CHSH correlator S achievable by any quantum state. Researchers in quantum foundations and Bell tests cite this constant to quantify the gap between the classical limit of 2 and the strongest observed violation. The declaration is a direct real-number assignment of 2 * Real.sqrt 2 that downstream lemmas then substitute into angle-specific correlation calculations.
Claim. The Tsirelson bound is defined by the equality $2√2$.
background
Recognition Science accounts for Bell violation through shared ledger entries: two particles created together inherit a common ledger record whose readout produces non-local correlations without signaling. The module QF-005 therefore replaces local-hidden-variable models with this ledger structure, recovering the classical CHSH bound |S| ≤ 2 while allowing the quantum value 2√2. The upstream definition in NonlocalityNoSignaling.tsirelsonBound already states the same numerical constant, so the present declaration simply re-exports it inside the BellInequality namespace for local use.
proof idea
One-line definition that directly assigns the value 2 * Real.sqrt 2.
why it matters
The definition is referenced by optimal_chsh_value to obtain S = -2√2 at the angles a=0, a'=π/2, b=π/4, b'=3π/4 and by quantum_violation to prove |optimalCHSH| = 2√2, thereby exhibiting the ledger-induced violation of the classical bound. It supplies the concrete number required by the QF-005 target of deriving Bell nonlocality from shared ledger entries. The value 2√2 is the Tsirelson bound, the standard quantum landmark separating classical from quantum correlations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.