rsObservables
plain-language theorem explainer
Packages the Recognition Science numerical predictions for three dimensionless observables: inverse fine-structure constant, electron-to-muon mass ratio, and proton-to-electron mass ratio. Downstream exclusivity and bridge lemmas cite this bundle as the concrete RS output of the cost-first ledger. It is a plain structure instance with fixed real literals, not a derived computation.
Claim. Define the RS observable triple $(\alpha^{-1},\, m_e/m_\mu,\, m_p/m_e)$ by the fixed values $\alpha^{-1} = 137.035999$, $m_e/m_\mu = 4.8363\times 10^{-3}$, and $m_p/m_e = 1836.15$.
background
In the exclusivity verification layer, a complete framework is asked to output a small bundle of dimensionless numbers only: inverse fine structure $\alpha^{-1}$, the electron-muon mass ratio, and the proton-electron mass ratio. The structure DimensionlessObservables is that bundle; every field is a real ratio with no SI anchor.
The module sits in the PredictionMap path that turns the RS cost functional $J$ and the golden ratio $\varphi$ into such a bundle. The companion Observables module records a parallel definition whose fields are named derived constants rather than bare literals; both are meant as RS predictions to be checked against CODATA-style bounds.
Primer context: $\alpha^{-1}$ is required to land in a narrow band near $137.03$–$137.04$, and mass ratios sit on the $\varphi$-ladder via the yardstick formula. This definition supplies the concrete numerical target those checks use.
proof idea
No proof. The declaration is a noncomputable structure instance: three field assignments to decimal literals. There is no tactic block, no lemma application, and no reduction from $J$ or $\varphi$ at this site; those derivations live upstream under names such as alpha_inv_derived in the Observables module. Here the values are simply recorded as the RS reference point for bounds and predictor maps.
why it matters
This bundle is the concrete RS side of the exclusivity prediction map. rsPredictionMap returns it for every $(J,\varphi)$ input; rs_within_bounds and rs_within_micro_window assert it lies inside empirical windows; and bridge_B5_prediction_map_exists packages existence of a predictor with
$P.\mathrm{predict}(J,\varphi)=\texttt{rsObservables}$ and the within-bounds property.
That bridge discharges Open Problem 1 (existence of a computable map from cost and $\varphi$ to dimensionless observables inside bounds). The values sit in the RS $\alpha$ band and on the mass ladder landmarks from the forcing chain (T5–T6 $J$-uniqueness and $\varphi$). Downstream unit-state predictors also hard-wire this same triple as the only admissible output.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.