passes_CODATA2022
plain-language theorem explainer
The Recognition Science predicted interval for the inverse fine-structure constant contains the CODATA 2022 measured value. Experimentalists and auditors of the preregistered α⁻¹ claim cite this as the pass/fail gate against the 2022 recommended number. The proof unfolds the three definitions and discharges the two rational inequalities by numerical normalization.
Claim. The preregistered RS prediction interval for $\alpha^{-1}$ contains the CODATA 2022 measured value: if $I=[\ell,u]$ is the predicted interval and $m$ is the CODATA 2022 central value, then $\ell \le m \le u$.
background
This module is a verification test in the preregistered $\alpha^{-1}$ suite: it asks only whether the declared RS prediction interval contains the declared CODATA 2022 measurement. In RS-native units the inverse fine-structure constant is forced into a narrow band (primer: $\alpha^{-1}$ inside $(137.030, 137.039)$); the Prediction module packages that band as a concrete interval, and Measurement_CODATA2022 packages the 2022 recommended value as a real.
Interval containment is the standard Numerics predicate: a real $x$ lies in $I$ when $\mathrm{lo}(I)\le x\le\mathrm{hi}(I)$. The test is deliberately thin. Tightening of the prediction band itself is deferred to AlphaBounds; this file only checks the already-declared endpoints against the already-declared measurement.
proof idea
One short tactic proof. Unfold interval_contains, prediction, and measurement_CODATA2022 to expose two concrete rational (or decimal) inequalities, then close both sides with norm_num. No lemmas beyond definitional unfolding are required; the comment in the proof body states the intentional dumbness of the check.
why it matters
Preregistered verification is how RS turns the forced $\alpha^{-1}$ band into an auditable claim against external metrology. This theorem is the CODATA-2022 instance of that gate: if the prediction interval ever fails to contain the recommended value, the preregistered suite fails in Lean rather than in prose.
It sits under the Verification.Preregistered.AlphaInv stack (Prediction + Measurement_CODATA2022 + Core). The primer landmark it polices is the $\alpha^{-1}$ window $(137.030, 137.039)$. Downstream consumers are not yet wired in this graph (used_by is empty); the declaration is itself an end-of-chain audit artifact. Interval tightening and any stricter comparison live in AlphaBounds, not here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.