alpha_inv_em_band
plain-language theorem explainer
The RS inverse fine-structure constant lies strictly between 137.030 and 137.039. Anyone citing the electromagnetic rung of the gauge-coupling hierarchy scorecard uses this band. The proof is a one-line pairing of the two certified numeric inequalities for the closed-form α⁻¹ expression.
Claim. The Recognition Science inverse fine-structure constant satisfies $137.030 < \alpha^{-1}_{\mathrm{EM}} < 137.039$.
background
This module packages the three Standard Model gauge couplings as an RS-derived hierarchy with zero free parameters. The electromagnetic entry is the closed-form inverse fine-structure constant $\alpha^{-1}$ assembled from the $\varphi$-exponential formula (seed times a gap exponential), not a CODATA fit.
Upstream, alphaInv is the dimensionless RS expression $\alpha_{\mathrm{seed}},e^{-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}}}$ (equivalently the PRC form $44\pi,\exp(-w_8\ln\varphi/(44\pi))$). The module doc states the target band $\alpha^{-1}_{\mathrm{EM}}\in(137.030,137.039)$ as item 1 of the hierarchy. Interval numerics supply the strict lower and upper bounds used here.
The local setting is a scorecard: EM band, $\sin^2\theta_W=(3-\varphi)/6$, $\alpha_s=\varphi^{-3}/\pi$, and the cube-geometry gauge sum $12\pi$, all certified with no sorry.
proof idea
Term-mode constructor proof. The goal is a conjunction of two strict inequalities. It is discharged by pairing Numerics.alphaInv_gt (lower bound $>137.030$) with Numerics.alphaInv_lt (upper bound $<137.039$). No algebraic rewriting occurs at this site; the work lives in the interval lemmas on the closed-form alphaInv.
why it matters
This is the electromagnetic clause of the gauge-coupling hierarchy scorecard. Downstream, gaugeCouplingHierarchyScoreCardCert_holds builds the certificate record by setting alpha_em_band := alpha_inv_em_band alongside positivity and ordering facts for the weak angle and the EM-vs-weak comparison.
In the RS primer the same open interval is the canonical $\alpha^{-1}$ band. It anchors the claim that the three SM couplings are forced by the $\varphi$-ladder and cube geometry rather than fit. The upstream alphaInv doc still flags the exact IR value $\alpha^{-1}(0)=137.035999$ as an OPEN boundary condition; this theorem only certifies the coarser RS band used by the scorecard, not that CODATA pin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.