cos_three_pi_div_four
plain-language theorem explainer
The lemma establishes that cosine of three pi over four equals negative square root of two over two. Researchers computing maximal CHSH violation in Recognition Science's shared-ledger model cite this identity when evaluating correlation functions at the angle 3π/4. The proof is a one-line rewrite that reduces the argument via ring, applies the cosine subtraction formula, and substitutes the known value at π/4.
Claim. $cos(3π/4) = -√2/2$
background
The Quantum.BellInequality module derives Bell inequality violation from Recognition Science ledger structure. Entanglement is modeled as two particles sharing a ledger entry, which produces the singlet correlation E(a,b) = -cos(a-b) without allowing signaling. The CHSH combination S is formed from four such terms evaluated at optimal angles that include 3π/4.
proof idea
The proof is a one-line wrapper. It rewrites the argument 3π/4 as π - π/4 by ring, applies the identity cos(π - x) = -cos(x), and substitutes the standard value cos(π/4) = √2/2.
why it matters
This identity is used inside optimal_chsh_value to reach S = -2√2, saturating the Tsirelson bound. It supplies the final numerical step in the module's derivation of quantum nonlocality from shared ledger entries (QF-005). The result confirms that the ledger model reproduces the maximal quantum correlation strength.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.