MassRatioBounds
plain-language theorem explainer
MassRatioBounds records the CODATA 2022 three-sigma intervals for the electron-muon mass ratio and the proton-electron mass ratio. Researchers comparing Recognition Science mass predictions against laboratory data reference these values through the downstream mass_ratio_bounds definition. The declaration is a plain structure that hard-codes the numerical defaults and year tag.
Claim. The record type contains the electron-to-muon mass ratio bounds from $4.83633136×10^{-3}$ to $4.83633202×10^{-3}$, the proton-to-electron mass ratio bounds from $1836.15267310$ to $1836.15267376$, and the source year $2022$.
background
The ExternalAnchors module is the single quarantined location for empirical calibration data that enters Recognition Science from external sources. The module policy states that the cost-first core must not import this module, preserving a mechanical separation between pure derivations from the Recognition Composition Law and experimental comparison data. All entries carry the external_anchor attribute for audit.
proof idea
The declaration is a structure definition that directly supplies default real values for each bound field together with the CODATA year. No lemmas or tactics are invoked; it functions as a record constructor with the listed constants.
why it matters
This supplies the external anchor instantiated by the mass_ratio_bounds definition, which closes the calibration seam interface. It permits comparison of Recognition Science results, including those obtained from the phi-ladder mass formula, with measured values while keeping external data out of the RCL core. It supports validation against the eight-tick octave and D=3 without altering the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.