badPrediction
plain-language theorem explainer
A deliberately wrong constant prediction map on the unit state space, returning α⁻¹ = 100 (not ~137) and other off-target dimensionless ratios. Serves as the negative control for the exclusivity observables interface. Anyone proving that DerivesObservablesStrong is non-vacuous cites it. Construction is a structure instance: constant predict field plus trivial uniformity by rfl.
Claim. There is a prediction function on the unit state space whose constant output is the dimensionless tuple $(\alpha^{-1}, m_e/m_\mu, m_p/m_e, G m_e^2/(\hbar c)) = (100, 0.001, 1000, 10^{-45})$, independent of state.
background
The Observables module fixes a non-trivial meaning of "derives observables": a framework must emit concrete dimensionless numbers that can be checked against measurement. Tracked quantities are $\alpha^{-1}$, $m_e/m_\mu$, $m_p/m_e$, and the dimensionless Newton constant $G m_e^2/(\hbar c)$. Core predictions stay cost-first (from $\varphi$); empirical windows sit behind an external-anchor seam.
A PredictionFunction on a state space is a total map to that four-tuple together with a uniformity law: the prediction does not depend on which state is fed in, so the numbers are framework-determined rather than trajectory-dependent.
Recognition Science itself targets $\alpha^{-1}$ inside roughly $(137.030, 137.039)$. The present definition deliberately sits far outside that band and the other empirical windows, so later theorems can show the strong derives-observables predicate rejects it.
proof idea
Definitional structure instance, not a proof. The predict field is the constant function sending every unit state to the hard-coded wrong four-tuple. Uniformity is discharged by rfl because both sides are definitionally the same constant. No lemmas are applied.
why it matters
Without a concrete failing example, "derives observables" could be an empty filter. This definition is the witness that the strong predicate is substantive: bad_prediction_fails shows the constant wrong tuple lies outside empirical bounds, and bad_framework_fails_strong lifts that to $\neg\exists$ a prediction function whose outputs all pass withinBounds when the predictor is this one.
In the exclusivity track, that non-vacuity is the gate before claiming only cost-first RS-style derivations (phi-ladder masses, forced $\alpha$ band, eight-tick structure) clear the observables bar. It does not itself encode T5–T8; it only polices the verification interface those forcing results must eventually satisfy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.