MeasurementAngle
plain-language theorem explainer
Measurement directions are typed as real numbers to parameterize settings in the Bell inequality derivations from shared ledger entries. It is cited when defining correlation functions and CHSH combinations in the Recognition Science quantum module. The declaration is a direct abbreviation for the reals.
Claim. A measurement direction is a real number.
background
The module QF-005 derives Bell inequality violation from Recognition Science ledger structure. Entanglement arises from shared ledger entries between particles, enabling non-local correlations without faster-than-light signaling. Classical local hidden variable theories obey |S| ≤ 2 for the CHSH combination, while the quantum case reaches the Tsirelson bound of 2√2. Upstream constants fix the active edge count A = 1 and coherence energy φ^{-5}.
proof idea
This declaration is a one-line abbreviation that sets the measurement angle type equal to the real numbers.
why it matters
The type supports quantumCorrelation, chshCombination, perfect_anticorrelation and the boundedness theorem. It implements the core setup for QF-005 on ledger-based nonlocality, connecting to the Tsirelson bound and the Recognition framework's treatment of entanglement. Downstream results use it to prove the quantum violation of the classical CHSH bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.