quantumCorrelation
plain-language theorem explainer
The quantum correlation for the singlet state is defined by E(θ_A, θ_B) = -cos(θ_A - θ_B). Physicists computing CHSH values or Tsirelson bounds cite this when quantifying Bell violations for entangled spins. It is a direct definition that encodes the quantum prediction without further reduction.
Claim. The correlation function for an entangled singlet state satisfies $E(θ_A, θ_B) = -cos(θ_A - θ_B)$ for real measurement angles θ_A and θ_B.
background
The module addresses QF-006 on nonlocality without signaling via ledger consistency: entangled particles share ledger entries (producing nonlocal correlations) while local reads leave the distant party's observations unchanged. The quantum correlation function supplies the expectation value for spin measurements on the singlet state. Upstream, the identical definition appears in BellInequality as the function E(a, b) = -cos(a - b) for MeasurementAngle inputs.
proof idea
Direct definition that sets the value to -Real.cos(θ_A - θ_B). No lemmas or tactics are applied beyond the cosine expression itself.
why it matters
This definition supplies the input to chshCombination, optimal_chsh_value, perfect_anticorrelation, and quantum_correlation_bounded in the BellInequality module. It supplies the quantum side of Bell's theorem, where the correlation reaches 2√2 and violates the classical bound of 2. In the Recognition framework it illustrates ledger-driven nonlocality that remains consistent with no-signaling, consistent with the overall forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.