optimalCHSH
plain-language theorem explainer
The definition assembles the CHSH correlator S at the angles that achieve maximal quantum violation of the Bell inequality. Physicists studying nonlocality in ledger-based models cite it to quantify the Tsirelson bound of 2√2. It is formed by selecting the optimal angle quadruple and substituting directly into the CHSH combination expression.
Claim. $S = E(0, π/4) - E(0, 3π/4) + E(π/2, π/4) + E(π/2, 3π/4)$, where the four angles are the optimal measurement settings and $E$ is the quantum correlation function for the singlet state.
background
The module QF-005 derives Bell inequality violation from Recognition Science's shared ledger entries: two particles created together share a ledger entry, producing non-local correlations without signaling. The CHSH combination is the expression S = E(a,b) - E(a,b') + E(a',b) + E(a',b'), which any local hidden variable theory bounds by 2. Optimal angles are the quadruple (0, π/2, π/4, 3π/4) chosen to maximize the quantum violation up to the Tsirelson bound 2√2.
proof idea
The definition is a one-line wrapper that destructures the optimalAngles tuple and passes the four angles to the chshCombination function.
why it matters
This definition supplies the concrete S value at the Tsirelson bound for the downstream theorems optimal_chsh_value and quantum_violation, which establish |S| = 2√2 and thereby the ledger-induced violation of the classical CHSH bound of 2. It directly fills the QF-005 target of deriving Bell violation from shared ledger entries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.