optimal_chsh_value
plain-language theorem explainer
The declaration establishes that the CHSH correlator evaluated at the four optimal measurement angles equals the negative of the Tsirelson bound. Quantum foundations researchers and ledger-based models of entanglement would cite it to fix the exact magnitude of the quantum violation. The proof is a direct algebraic verification that substitutes four explicit cosine identities and normalizes the resulting expression.
Claim. With measurement angles $a=0$, $a'=π/2$, $b=π/4$, $b'=3π/4$, the CHSH combination $S$ satisfies $S = -2√2$, where $2√2$ denotes the Tsirelson bound.
background
The module treats entanglement as shared ledger entries between particles created together, yielding non-local correlations without faster-than-light signaling. The CHSH combination is the alternating sum of four quantum correlation functions, each given by the negative cosine of the relative angle in the singlet state. Upstream results on spectral emergence supply the discrete geometric scaffolding, while primitive distinction axioms reduce the setup to four structural conditions plus definitional facts.
proof idea
The proof unfolds the definitions of the CHSH value, optimal angles, the combination operator, the correlation function, and the Tsirelson bound. It then establishes four auxiliary cosine identities for the angle differences via negation and standard trigonometric reductions, substitutes the values, and finishes with ring normalization.
why it matters
This supplies the precise numerical value required by the downstream quantum_violation theorem, which shows that the absolute value reaches the Tsirelson bound and exceeds the classical limit of 2. It directly advances the QF-005 target of deriving Bell violation from the ledger structure. The result confirms the maximal quantum violation |S| = 2√2 obtained here from shared ledger correlations rather than Hilbert-space postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.