alpha_result_contains_exp
plain-language theorem explainer
The Recognition Science interval for the inverse fine-structure constant contains the CODATA 2022 experimental central value. Verification and phenomenology workers cite this when checking RS α⁻¹ against PDG/CODATA. The proof unfolds the containment predicate and the concrete comparison record, then discharges both strict inequalities by numeric normalization.
Claim. Let the RS prediction for $\alpha^{-1}$ be the open interval $(137.030,\,137.039)$ and let the CODATA 2022 central value be $137.035999177$. Then $137.030 < 137.035999177 < 137.039$.
background
This module is a quarantined verification layer: it imports experimental CODATA/PDG numbers and records informational comparisons, not certified derivation steps. The local object is a comparison record with an RS lower bound, RS upper bound, experimental central value, and experimental sigma.
Containment means the experimental central value lies strictly between the RS bounds. The RS band used here is the machine-verified interval $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$ already advertised in the module header and aligned with the framework alpha window $(137.030,,137.039)$.
Upstream, the comparison record hard-codes those RS endpoints together with CODATA 2022 $\alpha^{-1}_{\mathrm{exp}} = 137.035999177(21)$. The containment predicate is the pure arithmetic statement that the central value sits inside the open RS interval.
proof idea
One short tactic proof. Unfold the containment predicate and the α⁻¹ comparison record so the goal becomes the pair of strict inequalities $137.030 < 137.035999177$ and $137.035999177 < 137.039$. Discharge both by norm_num. No lemmas beyond definitional unfolding are required.
why it matters
This is the headline pass/fail check of the PDG comparison module: RS α⁻¹ contains experiment. The module doc states the status explicitly (RS interval contains the experimental value) and cites CODATA 2022 and PDG 2024. In the broader framework it anchors the advertised alpha band inside $(137.030,,137.039)$ against a real metrology number.
It does not feed further certified theorems in the current graph (no downstream uses), and it sits outside the forcing chain T0–T8. Its role is external audit: a machine-checked witness that the RS numerical window is not empty of the measured inverse fine-structure constant. Tension-in-sigma analysis lives in sibling material, not here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.