rs_derives_observables_strong
plain-language theorem explainer
Recognition Science satisfies the strong observables-derivation predicate: it supplies a prediction function whose dimensionless outputs (fine-structure inverse, mass ratios, dimensionless G) lie inside empirical bounds on the unit state space. Exclusivity and non-vacuity arguments for the verification interface cite this witness. The proof is a direct existential term pairing the unit prediction function with the already-proved within-bounds fact.
Claim. Recognition Science satisfies the strong derivation predicate on the unit state space: there exists a prediction function $pf$ such that for every state $s$, the predicted dimensionless observables $pf(s)$ lie within the empirical bounds (on $\alpha^{-1}$, $m_e/m_\mu$, $m_p/m_e$, and dimensionless $G$).
background
This module builds a non-trivial observables interface for physics frameworks. "Derives observables" is not a vacuous label: a framework must emit specific numerical predictions comparable to measurement. The tracked quantities are all dimensionless: $\alpha^{-1}$, the electron-muon mass ratio, the proton-electron mass ratio, and $G\cdot m_e^2/(\hbar c)$. That choice avoids SI-anchor dependence.
The module keeps a clean calibration seam. The cost-first core defines the observables type and the RS-native predictions from the $\varphi$-forcing chain (no external anchors). An external-anchor section imports CODATA-style bounds and the comparison predicate withinBounds. Validation uses anchors; core predictions do not.
The strong predicate DerivesObservablesStrong asks for a prediction function whose every output falls inside those empirical bounds. Random or badly calibrated frameworks fail it. Upstream forcing material (eight-tick period, $D=3$, gap and cost structure) is what feeds the RS-native numerical values that the within-bounds lemma already checks.
proof idea
Term-mode existential witness, not a tactic script. The proof packages two ingredients already in the module: the unit prediction function (the RS prediction map on the trivial state space Unit) and the lemma that RS dimensionless observables lie inside empirical bounds. The second component is the constant function sending every state to that within-bounds fact. No new arithmetic is done here; the theorem only assembles the $\exists$ pair required by the strong predicate.
why it matters
This is the positive half of the exclusivity observables track: RS itself meets the non-trivial derivation standard. Its sole direct consumer is bad_framework_fails_strong, which shows a deliberately wrong $\alpha^{-1}$ predictor fails the same predicate. Together they prove the interface is discriminating, not a rubber stamp.
In framework terms, the numbers being checked are the cost-first outputs tied to the forcing chain (T5 J-cost uniqueness, T6 $\varphi$ fixed point, T7 eight-tick, T8 $D=3$) and the RS-native constants band for $\alpha^{-1}$. The theorem does not re-derive those constants; it certifies that the already-derived dimensionless package clears the empirical gate, which is the verification step exclusivity arguments need before claiming competing frameworks are ruled out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.