alpha_inv_0
plain-language theorem explainer
Local name for the RS infrared inverse fine-structure constant α⁻¹(0), equal to the canonical Constants.alphaInv construction (~137.04). Scorecard lemmas and the running-ratio definition cite it as the q²=0 endpoint. The body is a one-line alias with no extra proof work.
Claim. Define $\alpha^{-1}(0)$ as the Recognition Science infrared inverse fine-structure constant (the assembled dimensionless expression equal to $\texttt{alphaInv}$).
background
This module scores the QED running of the fine-structure constant from $q^2=0$ to $q^2=M_Z^2$, the dominant radiative correction to electroweak mass predictions. RS forces $\alpha^{-1}(0)$ into the open interval $(137.030, 137.039)$ via the forcing chain; PDG supplies the empirical check $\alpha^{-1}(M_Z)=127.951\pm 0.009$, so the ratio band is $(0.933,0.935)$.
Upstream, Constants.Alpha.alphaInv is the canonical exponential resummation $\alpha_{\mathrm{seed}},e^{-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}}}$ (nothing fit to CODATA). Its doc notes the seed $4\pi\cdot 11$ is an identification and the exact IR value $137.035999$ remains an OPEN boundary condition. A parallel PRC form is $44\pi,\exp(-w_8\ln\varphi/(44\pi))$.
The present definition simply re-exports that constant under the scorecard name $\alpha^{-1}(0)$, so ratio and band lemmas can speak in physics notation without reopening the construction.
proof idea
One-line definitional alias: alpha_inv_0 is definitionally equal to alphaInv. No tactics, no lemmas, no arithmetic. Downstream inequalities (alpha_inv_0_gt, alpha_inv_0_lt) discharge the numerical band by invoking Numerics.alphaInv_gt and Numerics.alphaInv_lt after unfolding this name.
why it matters
Anchors the infrared end of the Alpha Running Correction Scorecard. Every ratio object (running_ratio, running_ratio_gt, running_ratio_lt, running_ratio_lt_one) and the certificate structure AlphaRunningCorrectionScoreCardCert (field alpha_0_band) quote it. The module claims the correction ratio is not a free parameter: it follows from RS particle content (3 charged leptons, 5 light quarks, W) via the 1-loop vacuum-polarization sum, and proves zero additional free parameters.
Framework landmark: the primer band $\alpha^{-1}\in(137.030,137.039)$ is exactly the interval this name feeds. The exact CODATA-matching IR value remains OPEN upstream; this def does not close that gap, it only packages the RS expression for the running analysis and the corrected-VEV check against PDG.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.