optimalCHSH
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 in Recognition Science
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.
scope and limits
- Does not prove the classical CHSH bound of 2.
- Does not derive the optimal angles from the ledger structure.
- Does not compute the quantum correlation function itself.
- Does not address experimental realizations or signaling constraints.
formal statement (Lean)
121noncomputable def optimalCHSH : ℝ :=
proof body
Definition body.
122 let (a, a', b, b') := optimalAngles
123 chshCombination a a' b b'
124
125/-- cos(3π/4) = -√2/2 -/