alpha_inv_0_gt

Recognition Science forces a narrow window for the low-energy inverse fine-structure constant: $\alpha^{-1}(0)\in(137.030,137.039)$, coming from the forcing chain rather than a fit. In this module that RS value is named $\alpha^{-1}(0)$ and is definitionally identical to the certified constant alphaInv from the numerics layer.

The module's job is the QED running scorecard from $q^2=0$ to $q^2=M_Z^2$. That running is the dominant radiative correction to electroweak mass predictions; the PDG value $\alpha^{-1}(M_Z)=127.951\pm 0.009$ then implies a correction ratio in $(0.933,0.935)$. Establishing the lower edge of the RS $\alpha^{-1}(0)$ band is the first half of pinning that ratio.

Upstream, alphaInv_gt already proves $137.030<\mathrm{alphaInv}$ by interval arithmetic on the gap term (using $\log\varphi>0.481$ and eight-tick weight bounds).

One-line term proof: unfold the local definition $\alpha^{-1}(0):=\mathrm{alphaInv}$ and apply the upstream numeric theorem Numerics.alphaInv_gt, which already establishes $137.030<\mathrm{alphaInv}$. No extra arithmetic is done here.

This is the lower half of the RS $\alpha^{-1}(0)$ band quoted in the primer (alpha inverse inside $(137.030,137.039)$). Downstream, alphaRunningCorrectionScoreCardCert_holds packages it with the matching upper bound into alpha_0_band, then combines that with the running-ratio band and the RS particle-content counts (3 charged leptons, 5 light quarks) to certify the whole scorecard with zero extra free parameters.

Without this inequality the correction ratio $\alpha^{-1}(M_Z)/\alpha^{-1}(0)$ cannot be forced into $(0.933,0.935)$, and the claim that the VEV corrected by RS-native $\alpha(0)$ lands in the PDG band fails to close. It is a small numeric hinge, but it is load-bearing for the running-correction half of the electroweak mass story.