perfect_anticorrelation
plain-language theorem explainer
When two particles created from a shared ledger entry are measured along the same direction, their outcomes antic correlate perfectly. Researchers modeling Bell tests via Recognition Science ledger structure would cite this to recover the singlet prediction before deriving CHSH violation. The proof is a one-line wrapper that unfolds the correlation definition and reduces by simplification.
Claim. For any real measurement direction $a$, the quantum correlation of the Bell pair satisfies $E(a,a)=-1$.
background
The module derives Bell inequality violation from Recognition Science ledger structure, where entanglement equals shared ledger entries between particles created together. MeasurementAngle is an abbreviation for the real line, standing for a measurement direction. quantumCorrelation computes the expectation value of the product of outcomes (+1 or -1) for the two particles under the given angles, using the singlet state implicit in the ledger factorization.
proof idea
The proof unfolds the definition of quantumCorrelation and applies the simp tactic, which reduces the expression directly to -1 using the algebraic properties of the singlet correlation.
why it matters
This result supplies the perfect anticorrelation needed to reach the Tsirelson bound in the CHSH combination defined later in the module. It fills the quantum side of the ledger-based explanation of Bell violation (QF-005), connecting to the shared-ledger nonlocality that replaces hidden variables while preserving no-signaling. The theorem sits between the ledger factorization upstream and the classical bound comparison downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.