unitPrediction
plain-language theorem explainer
A constant prediction map on the one-point state space that always returns the RS dimensionless observables (α⁻¹, mass ratios, dimensionless G). Exclusivity and verification proofs cite it as the witness that Recognition Science, even with trivial state, still emits a fixed observable bundle. The construction is a structure instance: constant function plus reflexivity for uniformity.
Claim. There is a prediction function on the unit type whose extract map sends every state to the RS dimensionless observables $(\alpha^{-1}, m_e/m_\mu, m_p/m_e, G\, m_e^2/(\hbar c))$, and whose values are independent of the chosen state.
background
The Observables module fixes a non-trivial interface for physics frameworks: deriving observables means emitting concrete dimensionless numbers that can be checked against measurement, not merely asserting that some constants exist. The tracked bundle is DimensionlessObservables: fine-structure inverse $\alpha^{-1}$, electron-muon and proton-electron mass ratios, and dimensionless gravitational coupling $G m_e^2/(\hbar c)$. All entries are pure ratios, so SI anchors stay out of the cost-first core.
A PredictionFunction on a state space is a total map from states to that bundle together with a uniformity law: the prediction is framework-determined, not state-dependent. RS fills the bundle via rsObservables, whose components are derived from the $\varphi$-cost structure (forcing chain T5–T6 and the RCL) rather than fitted to CODATA. External bounds live in a separate, marked anchor section.
The unit type is the minimal state space used to show that even a one-point framework can carry a fixed RS prediction.
proof idea
Structure instance, not a multi-step proof. The predict field is the constant function returning rsObservables on every inhabitant of Unit. Uniformity is immediate: for any two unit states the two sides are definitionally equal, discharged by rfl. No lemmas beyond the structure fields and the already-constructed RS observable values are required.
why it matters
This is the prediction witness plugged into rsDerivesObservables and the strong theorem rs_derives_observables_strong, which assert that RS on the unit state satisfies the non-trivial DerivesObservables predicate (prediction function plus empirical bounds). Downstream exclusivity arguments need a concrete, uniform map from framework state to the four dimensionless targets; the unit instance is the cleanest such map and shows that the claim does not depend on a rich dynamics, only on the cost-derived numbers. It sits on the verification side of the calibration seam: core values come from $\varphi$ and the forcing chain, while bounds comparison is deferred to the external-anchor layer. Without this constant map, the strong "RS derives observables" statements have no inhabitant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.