withinBounds
plain-language theorem explainer
Predicate that a dimensionless observables package lies inside CODATA windows for α⁻¹, m_e/m_μ, and m_p/m_e. Exclusivity and prediction-map theorems cite it to force frameworks to match experiment rather than emit arbitrary numbers. Pure definitional conjunction of six inequalities against external anchors; no proof content.
Claim. For a dimensionless observables package $O=(\alpha^{-1},\, m_e/m_\mu,\, m_p/m_e,\, G_{\mathrm{dim}})$, write $\mathrm{withinBounds}(O)$ when $\alpha^{-1}_{\mathrm{lo}}\le\alpha^{-1}\le\alpha^{-1}_{\mathrm{hi}}$, $(m_e/m_\mu)_{\mathrm{lo}}\le m_e/m_\mu\le(m_e/m_\mu)_{\mathrm{hi}}$, and $(m_p/m_e)_{\mathrm{lo}}\le m_p/m_e\le(m_p/m_e)_{\mathrm{hi}}$, with the six endpoints taken from CODATA empirical bounds.
background
The Observables module separates a cost-first core from an external-anchor seam. The core type is the four-field package of dimensionless ratios any complete framework should predict: fine-structure inverse $\alpha^{-1}$, electron-to-muon mass ratio, proton-to-electron mass ratio, and a dimensionless gravitational coupling. RS fills that package from $\varphi$ via the cost structure (no CODATA import).
The external-anchor half imports CODATA windows and compares predictions to them. This predicate is that comparison: it asks whether three of the four fields sit inside their empirical intervals. Module policy marks it as an external anchor so the cost-first derivation chain stays free of laboratory numbers.
Upstream, the RS package is the cost-derived fill of the same structure; the empirical lower/upper constants come from the anchors import. The primer's $\alpha^{-1}$ band $(137.030,137.039)$ is the conceptual target this check operationalizes.
proof idea
Definitional, not a theorem. The body is the conjunction of six real inequalities: each of $\alpha^{-1}$, $m_e/m_\mu$, and $m_p/m_e$ is bounded below and above by the corresponding CODATA endpoint constants. Unfolding replaces the predicate with that conjunction; downstream proofs discharge it by simp against the concrete RS numbers plus norm_num, or refute it for deliberately bad packages the same way.
why it matters
This is the non-triviality gate for "derives observables." The strong derivation predicate and its witness structure both quantify over prediction maps whose every output satisfies the predicate, so random or off-band frameworks fail. The bad-prediction and bad-framework theorems use exactly that failure to show the interface is not vacuous.
On the positive side, the calibration-seam theorem asserts the RS package meets the predicate, and the prediction-map bridge packages that fact as existence of a computable map from $(J,\varphi)$ into the bounded observables set (Open Problem 1, existence). That lands the exclusivity story: cost-first forcing produces numbers inside the CODATA windows for $\alpha^{-1}$ and the two mass ratios, tying T5/T6 ($J$-uniqueness and $\varphi$) to laboratory anchors without smuggling SI units into the core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.