mass_ratio_bounds
This definition supplies the CODATA 2022 numerical bounds for the electron-muon and proton-electron mass ratios as a concrete external anchor. Modules that compare Recognition Science predictions to measured data cite it to fix the calibration seam. The construction is a direct record instantiation using the structure defaults with no computation or lemmas.
claimThe mass ratio bounds are the structure holding the electron-muon ratio in the closed interval $[4.83633136, 4.83633202] times 10^{-3}$, the proton-electron ratio in $[1836.15267310, 1836.15267376]$, and the CODATA year fixed at 2022.
background
The module isolates all empirical calibration data so that the cost-first core of Recognition Science never imports measurements. Mass ratio bounds collect the ±3σ intervals for two key particle ratios drawn from CODATA 2022. Upstream calibration axioms normalize the second derivative of the cost functional at the origin in log coordinates, while nucleosynthesis tiers place physical densities on discrete phi-ladder rungs.
proof idea
The definition is a direct record construction that supplies the default field values for the two mass-ratio intervals and the CODATA year. No lemmas or tactics are invoked; the body is the empty record literal matching the structure signature.
why it matters in Recognition Science
It supplies the single quarantined external anchor that any downstream comparison module must import when testing Recognition Science outputs against experiment. The structure supports validation against the phi-ladder mass formula and the alpha band without contaminating the pure RCL derivation. No open questions are closed here; the definition simply materializes the policy separation stated in the module header.
scope and limits
- Does not derive any mass ratio from the recognition composition law or J-cost axioms.
- Does not propagate experimental uncertainties beyond the stated 3σ bounds.
- Does not include neutron-proton or other particle mass ratios.
- Does not update automatically when future CODATA revisions appear.
formal statement (Lean)
197def mass_ratio_bounds : MassRatioBounds := {}
proof body
Definition body.
198
199end MassRatios
200
201/-! ## Calibration Seam Interface
202
203**EXTERNAL ANCHOR SECTION**
204
205These structures provide a clean interface for modules that need to compare
206RS predictions to empirical values.
207-/
208
209/-- **EXTERNAL ANCHOR**: A complete set of external anchors for comparison. -/