tsirelson_bound_value
plain-language theorem explainer
The declaration fixes the Tsirelson bound at exactly 2√2 inside the Recognition Science ledger model of entangled correlations. Quantum foundations researchers cite it when quantifying the maximum CHSH violation achievable from shared ledger entries. The proof is a one-line reflexivity step on the preceding definition of the bound.
Claim. The Tsirelson bound on the CHSH correlator satisfies $2√2$.
background
The module derives Bell inequality violation from shared ledger entries between entangled particles, where non-local correlations arise because measurements read the same ledger record. The Tsirelson bound is introduced as the quantum upper limit |S| ≤ 2√2 on the CHSH combination, contrasting with the classical bound of 2. This rests on the definition tsirelsonBound := 2 * Real.sqrt 2 together with the optimal measurement angles a=0, a'=π/2, b=π/4, b'=3π/4 that saturate the value.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of tsirelsonBound.
why it matters
It pins the exact numerical value of the Tsirelson bound for all downstream calculations of quantum nonlocality from ledger structure, directly supporting the module target of deriving Bell violation without signaling. The result aligns with the Recognition Science treatment of shared entries and the paper proposition on quantum nonlocality from ledger structure. No open questions remain as the equality is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.