quantum_correlation_bounded
plain-language theorem explainer
Quantum correlation for the singlet state satisfies |E(a,b)| ≤ 1 for any real measurement angles a and b. Researchers deriving Bell inequality violations from Recognition Science ledger entries cite this to anchor the quantum side before comparing to classical bounds. The proof is a direct reduction to the elementary cosine bound after unfolding the correlation definition.
Claim. For any real numbers $a, b$ representing measurement angles, the absolute value of the quantum correlation $E(a,b) = -cos(a-b)$ satisfies $|E(a,b)| ≤ 1$.
background
MeasurementAngle is an abbreviation for the real numbers, used as a simplified model of a measurement direction. The quantumCorrelation function is defined as -Real.cos(a - b), giving the expectation value for the singlet state. The module develops Bell inequality violation from Recognition Science shared ledger entries for entangled particles, with this bound serving as the quantum mechanical anchor before CHSH and Tsirelson comparisons. Upstream results include the cosine-form definition of quantumCorrelation both here and in the NonlocalityNoSignaling module.
proof idea
The term-mode proof unfolds the definition of quantumCorrelation to obtain -cos(a-b). It applies simp to replace abs(-x) with abs(x), then invokes the standard lemma abs_cos_le_one to conclude the bound.
why it matters
This theorem supplies the basic |E| ≤ 1 limit required to set up the contrast between classical CHSH ≤ 2 and the quantum Tsirelson bound in the QF-005 module on Bell violation from ledger structure. It directly supports the paper proposition deriving quantum nonlocality from shared ledger entries. No downstream uses are recorded, but the result closes the elementary bound step before sibling declarations on optimal angles and CHSH combinations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.