rs_within_bounds
plain-language theorem explainer
Recognition Science dimensionless observables sit inside the stated empirical windows (fine-structure inverse and key mass ratios). Exclusivity and prediction-map arguments cite this as the external calibration anchor. The proof unfolds the bounds predicate on the concrete RS values and closes the inequalities by numeric normalization.
Claim. The Recognition Science dimensionless observables lie within the prescribed empirical bounds: each of $\alpha^{-1}$, the electron-to-muon mass ratio, and the proton-to-electron mass ratio falls inside its experimental interval.
background
In the exclusivity verification layer, a dimensionless observables package packages the RS predictions that can be compared to experiment without units: typically $\alpha^{-1}$ and selected mass ratios. The predicate "within bounds" asserts componentwise membership in fixed empirical intervals (CODATA-style windows hard-coded as lower/upper constants).
Those predicted numbers are the cost-first RS values, not free fits. Upstream, cost is the J-cost on positive ratios (or the derived cost of a multiplicative recognizer), and scales live on the $\varphi$-ladder $\varphi^k$. The local module builds a Predictor: a map from (cost, scale) to such an observables package, together with a proof that the image stays inside bounds.
This declaration is the pure calibration fact for the RS package itself: the concrete RS observables satisfy the bounds predicate, before any predictor wrapper is attached.
proof idea
Short tactic proof. simp unfolds the bounds predicate and the definition of the RS observables package, exposing a finite conjunction of concrete real inequalities between the derived constants and the hard-coded empirical endpoints. norm_num then discharges every inequality by closed numeric evaluation. No algebraic lemma about J or $\varphi$ is invoked at this step; the work is definitional unfolding plus arithmetic.
why it matters
This is the external anchor (calibration seam) that ties cost-first RS numbers to experiment. Downstream, the RS prediction map packages it as the within_bounds field of the concrete Predictor, and the existence bridge (Open Problem 1) is proved by exhibiting that map together with this fact: there is a computable map from $(J,\varphi)$ to dimensionless observables inside bounds.
The same fact is re-used as the boundedness witness in the DerivesObservables constructions for the unit framework, including the strong (non-trivial) form. Without it, exclusivity cannot claim that RS predictions are empirically admissible. Framework-wise it sits next to the forced $\varphi$ and J-uniqueness chain: the ladder and cost law produce the numbers; this theorem only certifies they land in the $\alpha^{-1}$ band and the mass-ratio windows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.