optimalAngles
plain-language theorem explainer
The definition supplies the four measurement angles a=0, a'=π/2, b=π/4, b'=3π/4 that saturate the Tsirelson bound for the CHSH correlator inside the Recognition Science ledger model of entanglement. A physicist working on derivations of quantum nonlocality from shared ledger entries would cite this tuple when evaluating chshCombination or unfolding the correlation function. The body is a direct four-tuple assignment of the conventional angles with no further computation or lemmas.
Claim. $(a, a', b, b') = (0, π/2, π/4, 3π/4)$
background
The module QF-005 derives Bell inequality violation from Recognition Science ledger structure, where entanglement corresponds to two particles created together sharing a single ledger entry that produces non-local correlations without faster-than-light signaling. The CHSH combination is formed from four correlation measurements E(a,b) etc., bounded by 2 under local realism and by 2√2 under the quantum (Tsirelson) limit. Upstream dependencies include the structure for, which records meta-realization properties required by self-reference axioms, and the ILG action S defined as S_EH[g] + PsiAction[g,ψ].
proof idea
This is a one-line definition that directly returns the tuple (0, π/2, π/4, 3π/4). No lemmas are applied and no tactics are used; the angles are the standard choice known to achieve maximal violation.
why it matters
The definition is invoked by optimalCHSH to compute the CHSH value and by optimal_chsh_value to prove equality with -tsirelsonBound. It supplies the concrete angles needed for the QF-005 target of deriving Bell violation from ledger structure, as outlined for a PRL paper on quantum nonlocality from ledger structure. In the broader framework it shows how shared ledger entries reproduce the Tsirelson bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.