EmpiricalBounds
plain-language theorem explainer
Record type holding CODATA 2022 experimental windows for three dimensionless ratios: α⁻¹, m_e/m_μ, and m_p/m_e. Verification and exclusivity arguments cite it when checking whether a framework's predictions sit inside measured bands. Pure data carrier with default field values; no proof obligation.
Claim. A structure of real endpoints: lower and upper bounds on $\alpha^{-1}$ (default $137.0359$–$137.0361$), on $m_e/m_\mu$ (default $4.836\times 10^{-3}$–$4.837\times 10^{-3}$), and on $m_p/m_e$ (default $1836.15$–$1836.16$), taken from CODATA 2022 $\pm 3\sigma$ windows.
background
The Observables module splits cleanly into a cost-first core and an external-anchor section. The core exposes only the type of dimensionless predictions (α⁻¹, electron–muon mass ratio, proton–electron mass ratio, and dimensionless G) and the RS-derived values forced from φ. External anchors import laboratory numbers so that predictions can be compared to measurement without contaminating the forcing chain.
This structure is the anchor package for those laboratory windows. Defaults are CODATA 2022 intervals (α⁻¹ at roughly ±3σ). They are deliberately not derived from J-cost, the Recognition Composition Law, or the T0–T8 chain; the module marks them as external so exclusivity claims remain honest about what is forced versus what is measured.
Upstream mass definitions (electron mass on rung 2, proton mass as valence plus binding) feed the RS side of the comparison, not these bounds.
proof idea
No proof. Structure declaration with six real fields and numeric defaults. Instantiation is by empty braces (all defaults) or by overriding individual endpoints. Downstream empiricalBounds is exactly that default inhabitant.
why it matters
Gives the verification layer a typed place to store experimental acceptance windows without smuggling CODATA into the cost-first core. The sole direct consumer is the default inhabitant empiricalBounds, which then supplies legacy aliases and the withinBounds predicate used to test whether RS observables land inside measurement.
In the exclusivity story this is the calibration seam: RS must still produce α⁻¹ inside the primer band near (137.030, 137.039) and the mass ratios from the φ-ladder; this structure only records what "inside experiment" means. It does not close any T0–T8 step; it makes the empirical half of "derives observables" checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.