withinBounds
plain-language theorem explainer
Predicate that an observable triple (α⁻¹, m_e/m_μ, m_p/m_e) lies inside fixed empirical windows used for RS verification. Cited by exclusivity and prediction-map lemmas that demand frameworks hit CODATA-scale bands. Pure definitional conjunction of six inequalities; no proof content.
Claim. For a dimensionless observable bundle $o = (\alpha^{-1},\, m_e/m_\mu,\, m_p/m_e)$, write $\mathrm{withinBounds}(o)$ when $137.0359 \le \alpha^{-1} \le 137.0361$, $4.836\times 10^{-3} \le m_e/m_\mu \le 4.837\times 10^{-3}$, and $1836.15 \le m_p/m_e \le 1836.16$.
background
In the exclusivity verification layer, a complete framework is judged by dimensionless ratios only: the inverse fine-structure constant $\alpha^{-1}$, the electron–muon mass ratio, and the proton–electron mass ratio. The structure DimensionlessObservables packages exactly those three real fields (no SI anchors).
The companion value rsObservables hard-codes the RS cost-first predictions ($\alpha^{-1} = 137.035999$, $m_e/m_\mu = 4.8363\times 10^{-3}$, $m_p/m_e = 1836.15$). The present predicate supplies the external empirical windows against which any such triple is checked. A parallel definition in the Observables module uses named CODATA lower/upper constants; here the windows are written as literal bounds for the prediction-map bridge.
Local setting is the PredictionMap module: it builds the bridge that a prediction map exists and that RS values sit inside these bands, feeding the strong “derives observables” exclusivity tests.
proof idea
Definitional, not a proved statement. The body is the six-literal conjunction of closed interval membership for the three components of the observable bundle. No lemmas, tactics, or algebraic reduction; unfolding the definition yields the inequalities directly.
why it matters
This predicate is the external anchor that makes exclusivity non-vacuous. Downstream, DerivesObservablesStrong and DerivesObservablesWitness require every predicted state to satisfy it; bad_prediction_fails and bad_framework_fails_strong show that deliberately wrong predictions fall outside, so the strong predicate rejects junk frameworks. On the positive side, rs_within_bounds, prediction_map_matches_bounds, and bridge_B5_prediction_map_exists use it to certify that the RS triple (and the prediction map built from it) lands inside the windows.
Framework-wise it ties the cost-first ledger outputs to the empirical $\alpha^{-1}$ band cited in the RS primer (roughly $137.03$–$137.04$) and to the mass-ratio side of the $\phi$-ladder mass formula. It does not itself derive the constants; it only states the acceptance region those derivations must hit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.