alphaInv_RS_lower_verified

The module Machine-Verified PDG Comparison is quarantined from the certified surface: it imports experimental CODATA/PDG numbers and records informational comparisons, not derivation steps. Its headline claim is that the RS interval $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$ contains the CODATA 2022 value $137.035999177(21)$.

The RS constant itself is the dimensionless assembly $\alpha^{-1} = \alpha_{\mathrm{seed}},e^{-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}}}$ (equivalently $44\pi,\exp(-w_8\ln\varphi/(44\pi))$), with no fit to CODATA. The lower edge used here is the fixed real $137.030$ from the preregistered $\alpha^{-1}$ interval prediction. Upstream, alphaInv_gt already proves that same numerical inequality by bounding the gap term via $\log\varphi > 0.481$ and a controlled seed.

One-line term proof: the goal $137.030 < \alpha^{-1}$ is definitionally the statement of the upstream theorem alphaInv_gt from Numerics.Interval.AlphaBounds, so the declaration is just that theorem under the local name for the RS lower edge. No new arithmetic is performed here.

Closes the lower half of the machine-verified RS $\alpha^{-1}$ band advertised in the module key result and in the framework primer (prediction window $(137.030, 137.039)$). Together with the matching upper-bound verification it underwrites the claim that the CODATA 2022 central value sits inside the RS interval. No downstream Lean consumers are recorded yet; the declaration is a verification ledger entry rather than a link in the forcing chain (T0–T8). The exact infrared boundary condition $\alpha^{-1}(0)=137.035999$ remains open in Constants.Alpha, so this only certifies the constructed transcendental against its preregistered floor, not a derivation of the experimental digit string.