DerivesObservables
plain-language theorem explainer
A Prop-valued interface saying a physics framework "derives observables": inverse fine-structure in a narrow band around 137.036, a default mass-ratio identity in the golden ratio, the RS-native link ℏ = C_lag·τ₀ with c = 1, positivity of a default α, and that measurement always returns some observable. Exclusivity and NoAlternatives authors cite it as the weak, shared predicate. It is a structure of five fields, not a proved theorem; several fields are intentionally near-vacuous and the module points to the strong replacement.
Claim. A physics framework $F$ (state space, evolution, observables, measurement) is said to derive observables when: (i) the locked inverse fine-structure constant satisfies $137.035 \le \alpha^{-1}_{\mathrm{lock}} \le 137.037$; (ii) for every real $\varphi$, the default mass-ratio package gives $\mu/e = \varphi$; (iii) the RS-native constants obey $\hbar = C_{\mathrm{lag}}\,\tau_0$ and $c = 1$; (iv) the default $\alpha(\varphi)$ is positive for all $\varphi$; (v) measurement is total: every state maps to some observable.
background
The module supplies shared framework definitions for NoAlternatives and necessity arguments, so those developments do not import each other. A physics framework is the minimal interface: a state space, an evolution map, an observable type, a measurement map from states to observables, and existence of initial data.
Observable derivation is the claim that such a framework actually predicts dimensionless numbers and constant relations rather than merely having a measurement map. The alpha lock band here is a coarse interval around the empirical $\alpha^{-1}\approx 137.036$; the primer's tighter RS band is $(137.030,137.039)$. Mass content is routed through the RecogSpec default mass-ratio package evaluated at a real parameter $\varphi$ (intended as the golden ratio in RS).
Constants are the RS-native ones: $C_{\mathrm{lag}}=\varphi^{-5}$, $\tau_0$ the fundamental tick, $\hbar:=C_{\mathrm{lag}}\cdot\tau_0$, and $c=1$. The structure replaces an older vacuous existential "some positive $c,\hbar,G$" with this concrete link. SI/CODATA calibration sits outside this predicate.
proof idea
No proof body: this is a structure defining a proposition by five named fields. Inhabiting it means supplying evidence for each field (inequalities on the locked $\alpha^{-1}$, the mass-ratio identity, the two constant equations, positivity of default $\alpha$, and totality of measure). Downstream code that needs a non-trivial test should not unfold these fields; the module note redirects to DerivesObservablesStrong and explicit prediction functions in Observables.lean.
why it matters
This is the weak shared gate in Verification.Exclusivity: ParameterCount sits beside it in the same framework file, and Observables builds PredictionFunction, the RS witness rsDerivesObservables, and the non-triviality test bad_framework_fails_strong against the strong upgrade. The doc-comment and trailing note mark the structure deprecated for exclusivity: several conjuncts are always true once measurement is a function and defaults are fixed, so it cannot separate RS from a "bad" framework.
In the broader RS picture it still records the intended observable targets tied to the forcing chain: $\varphi$-ladder mass ratios, $\hbar=\varphi^{-5}$ in native units ($C_{\mathrm{lag}}\cdot\tau_0$), $c=1$, and an $\alpha^{-1}$ lock near 137.036. Non-circular exclusivity is supposed to use ExclusivityConstraints with DerivesObservablesStrong (empirical windows on $\alpha^{-1}$, $m_e/m_\mu$, $m_p/m_e$) instead of this trivial predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.