DerivesObservablesStrong
plain-language theorem explainer
A framework derives observables in the strong sense when a total, state-independent prediction map from its state space lands inside empirical CODATA bands on the canonical dimensionless set. Exclusivity and zero-parameter audits cite this predicate as the non-trivial gate. The body is a pure existential Prop: some prediction function whose every output satisfies the within-bounds check. Counterexample frameworks with wrong numbers fail it.
Claim. For a nonempty state space $S$, the strong derivation predicate holds iff there exists a prediction function $P:S\to\mathcal{O}$ that is constant on $S$ and such that for every $s\in S$, the dimensionless observables $P(s)$ lie inside the empirical bands on $\alpha^{-1}$, $m_e/m_\mu$, $m_p/m_e$, and the dimensionless Newton constant $G m_e^2/(\hbar c)$.
background
The module builds a non-trivial observables interface for physics frameworks. "Derives observables" is required to mean concrete numerical predictions comparable to measurement, not a vacuous flag. Calibration is split: the cost-first core defines the pure type of dimensionless observables and the RS values forced from $\varphi$; the external-anchor section imports CODATA bounds and the comparison predicate.
The tracked quantities are all dimensionless ratios: $\alpha^{-1}$, $m_e/m_\mu$, $m_p/m_e$, and $G\cdot m_e^2/(\hbar\cdot c)$. A prediction function on a state space $S$ is a total map $S\to\mathcal{O}$ that is uniform (framework-determined, independent of which state is fed in). The within-bounds predicate checks each component against CODATA intervals.
Upstream, several Observable notions exist (cost-structure recognition events, RS-native measurements, self-adjoint operators, bridge displays). This definition sits at the exclusivity layer and only uses the dimensionless bundle plus the prediction-function structure.
proof idea
Definitional, not a proved theorem. The body is the Prop $$\exists,P:\mathrm{PredictionFunction}(S),;\forall s\in S,;\mathrm{withinBounds}(P.\mathrm{predict},s).$$ No tactics or lemmas fire at the definition site. Downstream proofs discharge it by exhibiting a concrete witness (e.g. the unit-state RS prediction map) and invoking the RS-within-bounds lemma, or refute it by reducing to the bad-prediction failure lemma.
why it matters
This is the non-trivial gate that replaced the deprecated Framework-level derivation flags (those only locked a narrow $\alpha^{-1}$ window or a schematic mass-ratio identity and were always satisfiable in weak form). Downstream, rs_derives_observables_strong shows Recognition Science meets the predicate on the unit state space via the $\varphi$-forced observables; bad_framework_fails_strong and bad_prediction_fails prove a deliberately wrong predictor does not. Framework.DerivesObservables and ParameterCount point here for exclusivity bookkeeping.
In the RS chain the numbers being checked are the cost-first outputs (T5 J-uniqueness, T6 $\varphi$ fixed point, mass ladder, $\alpha^{-1}$ band near $137.03$–$137.04$), compared only at the external-anchor seam. The definition therefore separates "forced prediction" from "matches experiment" without smuggling SI units into the core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.