rsObservables
plain-language theorem explainer
Recognition Science packages its four dimensionless predictions (fine-structure inverse, electron-to-muon mass ratio, proton-to-electron mass ratio, and dimensionless G) into one record built from φ via the cost structure. Exclusivity and CODATA-compatibility arguments cite this bundle as the cost-first prediction vector. The definition is a pure structure instance wiring four already-derived constants; no proof obligations.
Claim. The RS-predicted observables are the four-tuple $(\alpha^{-1},\, m_e/m_\mu,\, m_p/m_e,\, G_{\mathrm{dim}})$ whose components equal the $\varphi$-derived fine-structure inverse, electron-to-muon mass ratio, proton-to-electron mass ratio, and dimensionless gravitational coupling $G\, m_e^2/(\hbar c)$.
background
The module defines a non-trivial observables interface: a framework "derives observables" only if it emits concrete dimensionless numbers comparable to measurement. The tracked quantities are $\alpha^{-1}$, $m_e/m_\mu$, $m_p/m_e$, and $G, m_e^2/(\hbar c)$. All are pure ratios, so no SI unit anchors enter the core.
A clean calibration seam splits the file. The cost-first core holds only the type DimensionlessObservables and the RS prediction record built here. The external-anchor section later imports CODATA 2022 bounds and comparison predicates, each tagged for mechanical audit. Core predictions must come from the forcing chain (J-cost uniqueness, $\varphi$ as self-similar fixed point), not from fitted constants.
Upstream cost infrastructure (observer J-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsened total cost) supplies the ledger language from which the four component values are computed. Those components are sibling definitions in this module; this declaration only assembles them.
proof idea
Definitional structure instance, not a proof. The four fields of the dimensionless-observables record are assigned to the four sibling derived constants (fine-structure inverse, electron-muon ratio, proton-electron ratio, dimensionless G). No tactics, no lemmas discharged at this site; the mathematical content lives in those component definitions and in the upstream cost/forcing chain that produces them.
why it matters
This record is the cost-first prediction vector that exclusivity arguments compare to experiment. Downstream, rs_within_bounds proves the four components lie inside CODATA 2022 windows (an external-anchor theorem bridging core predictions to measurement). The same bundle is the constant output of unitPrediction and of the RS prediction map, and it witnesses Open Problem 1 in bridge_B5_prediction_map_exists: there exists a computable map from $(J,\varphi)$ to dimensionless observables within bounds.
In framework terms it sits after the forcing chain landmarks that fix $J(x)=(x+x^{-1})/2-1$ and $\varphi$, and it feeds the exclusivity claim that RS is not an empty formalism. The $\alpha^{-1}$ slot is the natural place to confront the RS alpha band $(137.030,,137.039)$. Without this packaged prediction, the within-bounds and prediction-map existence results have nothing concrete to point at.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.