empiricalBounds
plain-language theorem explainer
Default CODATA-2022 window for the four dimensionless observables tracked by the exclusivity interface: α⁻¹, m_e/m_μ, m_p/m_e, and dimensionless G. Anyone checking RS (or a rival) against experiment cites this record. It is the empty-structure instance that inherits the structure's field defaults; no proof work.
Claim. Let $B$ be the default empirical-bounds record with CODATA-2022 $\pm 3\sigma$ windows: $\alpha^{-1}\in[137.0359,137.0361]$, $m_e/m_\mu\in[4.836\times 10^{-3},4.837\times 10^{-3}]$, and the corresponding proton-electron and dimensionless-$G$ intervals. Then $B$ is the canonical external anchor used by the within-bounds predicate.
background
The Observables module splits a cost-first core from an external-anchor seam. The core exposes only the type DimensionlessObservables and the RS-derived values rsObservables (α⁻¹, mass ratios, dimensionless G built from φ via the forcing chain). The seam imports CODATA numbers so that predictions can be compared to measurement without smuggling SI units into the derivation.
EmpiricalBounds is that seam's data type: four closed real intervals (lower/upper for each tracked observable), documented as CODATA 2022 and marked external. Field defaults already encode the ±3σ windows (e.g. α⁻¹ in [137.0359, 137.0361]). The present declaration is simply the default inhabitant of that structure.
Downstream predicates such as withinBounds read these fields; legacy top-level aliases (alpha_inv_lower, …) re-export them for older call sites. None of this is part of the T5–T8 cost-first chain; it is pure calibration data.
proof idea
Definitional, not a proof. The body is the empty structure instance {}, which fills every field of EmpiricalBounds from its default values (CODATA lower/upper bounds). No lemmas, no tactics, no computation beyond structure elaboration.
why it matters
This record is the experimental side of the calibration seam. The theorem rs_within_bounds shows that cost-first RS predictions (rsObservables, including the α⁻¹ band near 137.03x forced by the Recognition Composition Law and φ) land inside these CODATA windows; bad_prediction_fails shows a deliberately wrong predictor does not. Together they make "derives observables" a substantive claim: numerical match to measurement, not a vacuous typeclass.
In framework terms it anchors the exclusivity argument without contaminating the forcing chain (T5 J-uniqueness, T6 φ, T7 eight-tick, T8 D=3). The core stays pure; only the comparison predicate touches this external anchor. Referees checking the α band or mass-ratio ladder against CODATA start here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.