DimensionlessObservables
plain-language theorem explainer
A four-field record of dimensionless physics targets any complete framework must predict: α⁻¹, m_e/m_μ, m_p/m_e, and a Planck-scale dimensionless G. It is the pure type (no CODATA, no SI anchors) used by the exclusivity layer to state what "derives observables" means. Citation target for anyone wiring prediction functions or bounds checks. Definition only; no proof content.
Claim. A dimensionless observables package is a 4-tuple $(\alpha^{-1},\, m_e/m_\mu,\, m_p/m_e,\, G_{\mathrm{dim}})$ of real numbers, where $\alpha^{-1}$ is the inverse fine-structure constant, $m_e/m_\mu$ and $m_p/m_e$ are mass ratios, and $G_{\mathrm{dim}}$ is a dimensionless gravitational coupling (Planck-scale form $G\, m_e^2/(\hbar c)$). No external calibration data is part of the type.
background
The Observables module builds a non-trivial interface for physics frameworks: "derives observables" must mean concrete numerical predictions comparable to measurement, not a vacuous existence claim. It enforces a clean calibration seam. The cost-first core holds only pure types and RS predictions from the φ-based forcing chain (RCL → J-cost → φ → numbers). External anchors (CODATA bounds, within-bounds checks) live in a separate section marked as such.
The four tracked quantities are all ratios, so SI unit anchors never enter the type. Upstream, mass rungs and species data (electron, muon) and the recognition cost $J(x)=(x+x^{-1})/2-1$ supply the language in which RS later fills the fields; the structure itself does not compute them.
Local convention: this declaration is only the carrier type. Sibling defs supply RS-derived field values and empirical interval predicates.
proof idea
No proof. The declaration is a structure (record type) with four ℝ fields and field doc-comments. Namespace and later section comments only document the intended cost-first derivation chain; they are not part of this definition's body.
why it matters
This type is the payload of the exclusivity observables track. Downstream, PredictionFunction maps a framework state space into this record (with a uniformity condition that predictions are framework-determined, not state-dependent). DerivesObservablesStrong and DerivesObservablesWitness require some prediction function whose outputs lie in empirical bounds; rsDerivesObservables and rs_derives_observables_strong show RS meets that bar via rsObservables and rs_within_bounds.
The negative tests matter as much as the positive ones: bad_prediction_fails and bad_framework_fails_strong show that wrong numbers fail the strong predicate, so the interface is not vacuous. In framework terms this sits after the forcing chain landmarks (T5 J-uniqueness, T6 φ, mass ladder) and before exclusivity claims that only RS-style cost-first predictions clear the dimensionless target set. It does not itself close any open numerical gap; it only names the comparison surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.