electron_muon_ratio_CODATA
plain-language theorem explainer
The declaration supplies the CODATA 2022 central value for the electron-to-muon mass ratio as a fixed external calibration point. Researchers validating Recognition Science mass ladders against lepton data would cite this anchor when constructing comparison structures. It is introduced by direct assignment of the measured number in a quarantined module that the cost-first core is forbidden to import.
Claim. The electron-to-muon mass ratio is defined by the constant value $m_e/m_μ = 4.83633169 × 10^{-3}$.
background
The module ExternalAnchors is the single location permitted to hold empirical calibration data that enters Recognition Science from outside the RCL derivation. Its policy isolates all CODATA values so that the pure cost-first core (IndisputableMonolith.Cost) never imports them, while any downstream module that does import the anchors explicitly acknowledges the external seam. This particular definition records the 2022 CODATA central value for the lepton mass ratio without uncertainty or derivation.
proof idea
The declaration is a direct noncomputable definition that performs a literal assignment of the numerical constant; no lemmas, tactics, or reductions are applied.
why it matters
It supplies the electron_muon field inside the EmpiricalAnchors structure, which collects all external anchors for side-by-side numerical checks against RS-native constants. The placement enforces the mechanical separation between the RCL primitive and laboratory data, allowing later comparison of the phi-ladder mass formula against measured lepton ratios while keeping the core derivation untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.