quantum_violation
plain-language theorem explainer
The theorem establishes that the CHSH correlator at optimal angles equals the Tsirelson bound of 2√2, exceeding the classical limit of 2. Quantum foundations researchers would cite this for the Recognition Science ledger derivation of Bell violation. The proof is a term-mode reduction that rewrites to the optimal value then applies absolute-value and positivity lemmas to reach the equality.
Claim. For optimal measurement angles the absolute value of the CHSH combination satisfies $|S| = 2√2$.
background
Recognition Science treats entanglement as arising from shared ledger entries created when two particles are produced together. The CHSH combination is defined as $S = E(a,b) - E(a,b') + E(a',b) + E(a',b')$, where each $E$ is a correlation function. Classical local realism requires $|S| ≤ 2$, while the Tsirelson bound reachable by quantum mechanics is $2√2$. The module derives the violation directly from the ledger structure without invoking hidden variables or faster-than-light signaling.
proof idea
The proof is a one-line term-mode wrapper. It rewrites the optimal CHSH value, applies abs_neg and abs_of_pos to handle the sign, then invokes mul_pos together with Real.sqrt_pos to confirm the positive square-root expression equals $2√2$.
why it matters
This result completes the QF-005 derivation of Bell violation inside the Recognition Science framework. It supplies the concrete numerical prediction that feeds the ledger-based account of nonlocality and supports the planned PRL paper on quantum nonlocality from ledger structure. The equality anchors the quantum side of the CHSH comparison and closes the gap between the classical bound of 2 and the observed violation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.