mass_ratio_bounds
plain-language theorem explainer
mass_ratio_bounds supplies the CODATA 2022 empirical bounds on the electron-muon and proton-electron mass ratios for use in Recognition Science calibration comparisons. Any module importing ExternalAnchors acknowledges use of external data. The definition is a direct instantiation of the MassRatioBounds structure with the listed interval endpoints and year tag.
Claim. The empirical mass ratio bounds are the structure with electron-muon ratio in the closed interval $[4.83633136, 4.83633202]times 10^{-3}$, proton-electron ratio in $[1836.15267310, 1836.15267376]$, and codata_year equal to 2022.
background
The ExternalAnchors module is the single quarantined location for all empirical calibration data entering Recognition Science. Its policy states that the cost-first core must not import this module, creating a mechanical separation between pure RCL derivation and external comparison values. All definitions carry the @[external_anchor] tag for audit.
proof idea
One-line definition that directly constructs the MassRatioBounds structure using its declared default field values; no lemmas, tactics, or upstream results are invoked beyond the structure literal itself.
why it matters
This declaration populates the external anchor interface for mass ratios, enabling modules that import ExternalAnchors to compare RS predictions (such as phi-ladder mass formulas) against CODATA 2022 data. It completes the calibration seam described in the module documentation after CostAxioms.Calibration and CostFromDistinction.Calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.