bad_framework_fails_strong
plain-language theorem explainer
A framework that emits deliberately wrong dimensionless observables (α⁻¹ = 100, off mass ratios, wrong dimensionless G) fails the strong derives-observables predicate. Cite this when arguing the exclusivity observables interface is non-vacuous. Proof is a one-line unpack of the existential, then apply the already-proved out-of-bounds lemma on those numbers.
Claim. There is no prediction function on the unit state space such that, for every state, the fixed wrong observable tuple $\alpha^{-1}=100$, $m_e/m_\mu=0.001$, $m_p/m_e=1000$, $G_{\mathrm{dim}}=10^{-45}$ lies inside the empirical bounds. Equivalently, a framework locked to those bad predictions does not satisfy the strong derives-observables property.
background
This module defines a non-trivial observables interface for physics frameworks. "Derives observables" must mean producing concrete dimensionless numbers checkable against measurement, not a vacuous existence claim.
The tracked quantities live in DimensionlessObservables: fine-structure inverse $\alpha^{-1}$, electron-muon mass ratio, proton-electron mass ratio, and dimensionless gravitational coupling $G\cdot m_e^2/(\hbar c)$. A PredictionFunction on a state space is a total, state-independent map into that structure. The strong predicate asserts existence of such a function whose outputs all satisfy withinBounds (CODATA-anchored intervals, marked as external anchors).
The older Framework.DerivesObservables structure is deprecated as always-satisfiable. The counterexample badPrediction hard-codes $\alpha^{-1}=100$ and other wrong values. Upstream, bad_prediction_fails already shows those four numbers fail the empirical lower/upper cuts.
proof idea
Short term-mode proof by contradiction. Unpack the existential (a dummy PredictionFunction on Unit plus the claim that badPrediction.predict lands in bounds at every unit state). Specialize that claim at the unique inhabitant (), then finish with bad_prediction_fails, the direct Boolean out-of-bounds check on the four numerical components against the empirical bound constants.
why it matters
Supplies the negative half of the module summary: RS satisfies the strong derives-observables predicate, while a wrong-prediction framework fails it. That pair replaces the old always-satisfiable DerivesObservables interface (loose $\alpha^{-1}$ locks plus a mass-ratio placeholder). Without this failure theorem, exclusivity arguments could not claim that "derives observables" actually filters frameworks.
The planted $\alpha^{-1}=100$ sits far outside both the RS alpha band $(137.030, 137.039)$ and the CODATA window used by withinBounds. No downstream theorem currently depends on this lemma (used_by is empty); it stands as the explicit non-triviality witness in the module's closing summary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.