chshCombination
plain-language theorem explainer
chshCombination assembles the CHSH correlator S from four quantum correlation values at chosen angles. Researchers deriving Bell violations from shared ledger entries in Recognition Science cite it when evaluating maximal quantum correlations. The definition is a direct linear combination of the four quantumCorrelation terms.
Claim. $S(a,a',b,b') = E(a,b) - E(a,b') + E(a',b) + E(a',b')$ where each $E$ denotes the singlet correlation function $E(a,b) = -cos(a-b)$ and each angle is a real number.
background
The BellInequality module derives quantum nonlocality from shared ledger entries that encode entanglement in Recognition Science. MeasurementAngle is an abbreviation for a real number that parametrizes a measurement direction. quantumCorrelation supplies the singlet expectation $E(a,b) = -cos(a-b)$. The module setting contrasts the classical local-hidden-variable bound |S| ≤ 2 with the quantum Tsirelson bound 2√2.
proof idea
This is a definition that directly assembles the signed sum of four quantumCorrelation applications at the supplied angle pairs.
why it matters
It supplies the input to optimalCHSH and the theorem optimal_chsh_value that recovers S = -2√2. The construction therefore supports the module claim that ledger sharing produces the Tsirelson violation of the classical CHSH bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.