tsirelsonBound
plain-language theorem explainer
The Tsirelson bound fixes the maximum quantum violation of the CHSH inequality at 2√2. Researchers in quantum foundations cite this constant to quantify the separation between classical limits of 2 and achievable quantum correlations. The declaration supplies the value as a direct real-number constant imported from the Bell inequality analysis.
Claim. The quantum Tsirelson bound equals $2 sqrt{2}$.
background
Recognition Science resolves the tension between quantum nonlocality and no-signaling by positing a shared ledger that maintains global consistency for entangled particles while restricting access to local readings. Entangled systems share ledger entries, producing correlations that violate Bell inequalities, yet one party's measurement leaves the other's observable statistics unchanged. The module imports the Tsirelson bound from the BellInequality module, where it is defined as the same constant 2 * Real.sqrt 2 and documented as the maximum quantum value of the CHSH correlator S.
proof idea
The declaration is a direct definition that assigns the constant value 2 * sqrt 2 to the Tsirelson bound.
why it matters
This constant supplies the exact violation magnitude used by optimal_chsh_value and quantum_violation to show |S| = 2√2, and by bell_violation to establish the breach of the classical chshBound. It anchors the ledger-consistency argument in QF-006 by giving the precise strength of nonlocal correlations while the no_signaling_theorem blocks information transfer. The placement aligns with the recognition composition law governing correlation structures and the eight-tick octave that sets the periodicity of quantum measurements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.