DerivesObservablesWitness
plain-language theorem explainer
Packages a non-empty state space with a total, state-independent prediction map into the four canonical dimensionless observables, plus a certificate that every prediction lands inside empirical bounds. Exclusivity and framework-comparison arguments cite it as the witness that a theory actually derives numbers rather than merely naming them. As a structure definition there is no proof body; instances are built by supplying the prediction function and the bounds proof.
Claim. For a nonempty state space $S$, a derivation witness consists of a total map $P:S\to\mathcal{O}$ into the four dimensionless observables $(\alpha^{-1},\,m_e/m_\mu,\,m_p/m_e,\,G m_e^2/(\hbar c))$ that is constant on $S$, together with a proof that $P(s)$ lies inside the empirical bounds for every $s\in S$.
background
The Observables module fixes what it means for a physics framework to derive observables in a non-trivial way: it must emit specific dimensionless numbers comparable to measurement. The tracked set is $\alpha^{-1}$, the electron-muon mass ratio, the proton-electron mass ratio, and the dimensionless gravitational coupling $G m_e^2/(\hbar c)$. All four are pure ratios, so SI anchor choices never enter the core type.
A calibration seam splits the module. The cost-first core defines the observable record and the RS predictions obtained from the $\varphi$-forcing chain. External anchors (CODATA) appear only in the empirical-bounds record and the within-bounds predicate, both tagged as external. A prediction function on a state space is required to be total and uniform: every state yields the same observable tuple, so the numbers are framework-determined rather than state-dependent.
This witness structure is the packaged form of that requirement: prediction map plus bounds certificate, parameterized by any nonempty state space.
proof idea
No proof body: the declaration is a structure. An instance is assembled by giving a PredictionFunction (a uniform map from states into the four-observable record) and a proof that every predicted tuple satisfies the within-bounds predicate against the external empirical envelope. Downstream, the RS instance on the unit state space fills both fields with the fixed RS prediction map and the already-proved RS-within-bounds fact.
why it matters
Exclusivity arguments need a hard criterion that separates frameworks which merely gesture at physics from those that output checkable numbers. This witness is that criterion. Its sole direct consumer is the RS derivation instance on the unit state space, which shows Recognition Science meets the strong derives-observables predicate.
The numbers themselves sit on the cost-first side of the calibration seam: $\alpha^{-1}$ in the RS band near $137$, mass ratios from the $\varphi$-ladder with the mass formula yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$, and dimensionless $G$ from the RS-native constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$. The structure therefore links the forcing-chain outputs (T5 J-uniqueness through the $\varphi$ fixed point) to the verification layer without smuggling SI units into the core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.