rsDerivesObservables
plain-language theorem explainer
Recognition Science, treated as a framework with trivial Unit state, supplies an explicit witness that it derives dimensionless observables inside empirical bounds. Anyone checking exclusivity or calibration of RS against CODATA cites this packing. The body just wires the constant Unit prediction map to the already-proved within-bounds theorem.
Claim. There is a witness that the Recognition Science framework on the trivial state space $\mathbf{1}$ derives observables: its prediction function returns the fixed RS dimensionless observables $(\alpha^{-1}, m_e/m_\mu, m_p/m_e, G m_e^2/(\hbar c))$, and those values lie inside the empirical CODATA bounds for every state.
background
The Observables module separates a cost-first core from external anchors. The core type DimensionlessObservables packages four dimensionless ratios any complete framework should predict: $\alpha^{-1}$, $m_e/m_\mu$, $m_p/m_e$, and $G m_e^2/(\hbar c)$. RS fills that type via cost-structure values derived from $\varphi$ (the self-similar fixed point forced at T6), without SI units.
Empirical comparison lives behind a calibration seam: EmpiricalBounds and withinBounds import CODATA 2022 ranges. The theorem rs_within_bounds asserts that the RS-derived tuple sits inside those ranges; it is marked as an external-anchor result.
DerivesObservablesWitness is the non-trivial interface: a framework must exhibit a prediction function on its state space and prove every prediction is within bounds. The older DerivesObservables Prop on PhysicsFramework is deprecated in favor of this witness form (and the strong predicate). unitPrediction is the constant map from Unit that always returns the RS observables.
proof idea
Definitional packing, not a tactic proof. The witness fields are filled by two prior objects: predictionFn is set to unitPrediction (the constant Unit map to rsObservables, with trivial uniformity), and bounded is the constant function that ignores the Unit state and returns rs_within_bounds. No new arithmetic is done here; the numerical work lives entirely in that upstream within-bounds theorem (simp plus norm_num against CODATA endpoints).
why it matters
Exclusivity arguments need a substantive meaning of "derives observables": numerical predictions comparable to measurement, not a vacuous Prop. This definition is the RS-side witness on the trivial state space, showing that even Unit state is enough once the cost-first $\varphi$-ladder values are fixed and checked against CODATA.
It sits at the calibration seam of the verification stack: core predictions come from the forcing chain (T5 J-uniqueness, T6 $\varphi$, mass ladder), while bounds are external. The module tracks the $\alpha^{-1}$ band near 137 and the standard mass ratios. Downstream exclusivity or strong-derivation predicates can consume this witness; the page currently lists no direct used_by edges, so it is an interface endpoint rather than an intermediate lemma.
No open scaffold remains in this declaration itself; any residual numerical tension would surface in rs_within_bounds or the derived observable defs, not here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.