rs_within_bounds
plain-language theorem explainer
Recognition Science dimensionless predictions (α⁻¹ and two mass ratios) sit inside CODATA 2022 windows. Exclusivity and prediction-map bridges cite it to certify a non-trivial “derives observables” witness. Proof unfolds the bound predicate and the derived values, then discharges the six inequalities by numerical normalization.
Claim. Let $O$ be the RS-derived dimensionless observables $(\alpha^{-1},\, m_e/m_\mu,\, m_p/m_e)$. Then each coordinate of $O$ lies in the corresponding open CODATA interval: $\alpha^{-1}_{\mathrm{lo}} < \alpha^{-1} < \alpha^{-1}_{\mathrm{hi}}$, and likewise for the electron–muon and proton–electron mass ratios.
background
This module separates a cost-first core from an external-anchor seam. The core builds a record of dimensionless observables (fine-structure inverse, electron/muon mass ratio, proton/electron mass ratio, and a dimensionless Newton constant) whose RS values are forced from the φ-ladder and J-cost structure, with no CODATA input. The anchor seam packages CODATA 2022 windows into an empirical-bounds record and a predicate that checks componentwise membership.
The calibration policy is explicit: core predictions stay pure; only the comparison predicate imports external numbers. All tracked quantities are dimensionless ratios, so SI unit anchors never enter. The present theorem is the seam that joins the two sides: it asserts that the RS record lands inside the empirical windows.
Upstream forcing (T5 J-uniqueness, T6 φ fixed point, mass ladder with rung gaps) is what produces the concrete RS numbers being checked; this lemma does not re-derive them.
proof idea
Tactic proof, not a deep algebraic argument. First simp only expands the within-bounds predicate, the RS observables record, and the three derived fields (α⁻¹, electron/muon, proton/electron). A second simp only unfolds the six CODATA endpoints and the empirical-bounds record. The goal is then six concrete real inequalities; norm_num closes them all. No upstream forcing lemmas are invoked at the call site: the numerical content is already baked into the derived constants.
why it matters
This is the external-anchor certificate that RS predictions are experimentally compatible. Downstream, the strong derives-observables witness for the unit framework is built by packaging a prediction function with this bound proof; the companion theorem that RS satisfies the strong predicate is the same packaging. In the prediction-map layer it discharges Open Problem 1 (existence): there is a computable map from (J-cost, φ) to dimensionless observables inside bounds, and the value-identification lemma that the RS map matches those bounds is a one-line appeal here.
Framework-wise it sits at the calibration seam after the forcing chain has fixed φ and the mass ladder. The α⁻¹ window is the same band the primer quotes near 137.03–137.04. It does not close uniqueness of the framework; it only shows the RS numbers clear the experimental gate that exclusivity arguments require.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.