DimensionlessObservables
plain-language theorem explainer
Packages three pure ratios any complete physics framework must predict: inverse fine-structure constant, electron-to-muon mass ratio, and proton-to-electron mass ratio. Exclusivity and verification arguments use this type as the common codomain of prediction maps. Plain structure definition; no proof obligations.
Claim. A dimensionless observable triple is a record of three real numbers $(\alpha^{-1},\, m_e/m_\mu,\, m_p/m_e)$: the inverse fine-structure constant, the electron-to-muon mass ratio, and the proton-to-electron mass ratio, with no SI unit anchors.
background
In the exclusivity layer, frameworks are compared by what dimensionless numbers they force, not by unit-dependent constants. The three fields here are the standard pure ratios: $\alpha^{-1}$ (fine-structure), $m_e/m_\mu$, and $m_p/m_e$. All are scale-free, so SI calibration cannot smuggle agreement.
Upstream mass infrastructure places $m_e$ on the $\varphi$-ladder (electron rung $r_e=2$, $m_e=E_{\mathrm{coh}}\cdot\varphi^2$) and treats $m_p/m_e$ as a structural $\varphi$-power once confinement is fixed. Recognition cost is the $J$-cost on positive ratios; the present bundle does not recompute those costs, it only names the observables they are asked to match.
The local module builds prediction maps from framework state spaces into this triple, then tests componentwise empirical windows. A parallel structure in Observables restates the same three fields as the canonical target set for any complete theory.
proof idea
No proof. The declaration is a three-field structure on $\mathbb{R}$: inverse fine-structure, electron-muon ratio, proton-electron ratio. Downstream predicates (bounds, micro-windows, prediction functions) pattern-match on these projections.
why it matters
This type is the shared codomain for exclusivity. PredictionFunction maps any state space into it and demands state-independent output. DerivesObservablesStrong and DerivesObservablesWitness assert existence of such a map whose values lie in empirical bounds; bad_prediction_fails and bad_framework_fails_strong show the strong predicate is non-vacuous by exhibiting a wrong triple that fails the windows.
In the RS programme the same three numbers are the cost-first ledger targets (alpha band near $137.03$--$137.04$, mass ratios from the $\varphi$-ladder). The structure itself carries no numerics; it only fixes the interface so that bridge theorems can compare RS predictions against rivals without unit ambiguity. It sits under the verification claim that a framework derives observables only if it hits this bundle inside bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.