bad_prediction_fails
plain-language theorem explainer
A deliberately wrong prediction of the four dimensionless observables falls outside the CODATA empirical windows. Anyone checking that the strong "derives observables" predicate is non-vacuous cites this fact. The argument unfolds the within-bounds predicate on the bad prediction and discharges the resulting numerical inequalities by arithmetic normalization.
Claim. The dimensionless observables produced by the bad prediction map do not satisfy the empirical bounds: they fail the conjunction of interval constraints on $\alpha^{-1}$, $m_e/m_\mu$, $m_p/m_e$, and the dimensionless gravitational coupling $G m_e^2/(\hbar c)$.
background
This module builds a non-trivial observables interface for physics frameworks. "Derives observables" is required to mean something substantive: the framework must emit specific numerical predictions that can be compared to measurement. The tracked quantities are all dimensionless ratios: $\alpha^{-1}$, $m_e/m_\mu$, $m_p/m_e$, and $G m_e^2/(\hbar c)$, so SI anchor issues are avoided.
A clean calibration seam separates the cost-first core from external anchors. The structure of dimensionless observables is a pure type (four real fields, no CODATA). Empirical bounds and the within-bounds predicate live in the external-anchor section and compare predictions to experiment. Recognition Science native predictions sit on the cost-first side; the validation side only checks whether a given four-tuple lands inside the measured windows.
The bad prediction is a fixed, intentionally wrong four-tuple used as a negative control. The theorem asserts that this control fails the within-bounds check.
proof idea
Tactic proof by simplification and numerical discharge. First unfold the within-bounds predicate and the bad prediction definition, exposing a conjunction of interval memberships. Then unfold the concrete lower and upper endpoints for $\alpha^{-1}$, the electron-muon ratio, and the proton-electron ratio, together with the empirical-bounds package. The resulting closed numerical inequalities are settled by norm_num. No external lemmas are required beyond definitional unfolding.
why it matters
This is the negative control that makes the strong observables predicate non-vacuous. Downstream, bad_framework_fails_strong quotes it directly: any framework whose prediction function always returns the bad four-tuple fails the strong "derives observables" existence claim. Without a concrete failing example, the exclusivity interface could accept arbitrary frameworks by vacuity.
In the broader Recognition verification stack, the positive side is that RS-native dimensionless values (forced from the cost structure and the $\phi$-ladder, with $\alpha^{-1}$ in the narrow band near 137) do sit inside the same windows. The present lemma is the matching failure case: wrong numbers are rejected. It does not itself derive $\alpha$ or the mass ratios; it only certifies that the comparison predicate has teeth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.