alpha_weak_inv
plain-language theorem explainer
Defines the inverse weak coupling as the product of the RS electromagnetic inverse fine-structure constant and the RS Weinberg angle factor sin²θ_W. Anyone checking the EM–weak hierarchy or the gauge scorecard cites this abbreviation. It is a one-line product of two already-named RS constants.
Claim. The inverse weak coupling is defined by $\alpha^{-1}_{\mathrm{weak}} := \alpha^{-1}_{\mathrm{EM}} \cdot \sin^2\theta_W$, where $\alpha^{-1}_{\mathrm{EM}}$ is the RS fine-structure expression and $\sin^2\theta_W = (3-\varphi)/6$.
background
The Gauge Coupling Hierarchy Scorecard module packages the three Standard Model gauge couplings as RS-forced quantities with zero free parameters. Electromagnetic strength sits in the narrow band $\alpha^{-1}_{\mathrm{EM}} \in (137.030, 137.039)$ from the $\varphi$-exponential formula; the weak sector is tied to EM by a fixed Weinberg angle; the strong coupling is $\alpha_s = \varphi^{-3}/\pi$ with gauge sum $12\pi$.
Upstream, alphaInv is the dimensionless inverse fine-structure constant (canonical exponential resummation, value near 137.04, nothing fit to CODATA). Independently, the PRC form writes $\alpha^{-1} = 44\pi,\exp(-w_8\ln\varphi/(44\pi))$. The angle factor is $\sin^2\theta_W = (3-\varphi)/6$, forced positive and strictly less than one because $\varphi < 2$.
This definition simply multiplies those two RS numbers to obtain the inverse weak coupling used in hierarchy comparisons.
proof idea
Pure definition: unfold to the product of the RS inverse fine-structure constant and the RS $\sin^2\theta_W$. No tactics, no lemmas, no proof obligations.
why it matters
Feeds the hierarchy theorem that electromagnetic inverse coupling strictly exceeds the weak one (because $\sin^2\theta_W < 1$), and appears as the comparison field inside GaugeCouplingHierarchyScoreCardCert. That certificate also records the EM band, positivity and upper bound on $\sin^2\theta_W$, and the gauge-sum identity equal to $12\pi$.
In the broader RS chain this sits under the forced constants picture: $\alpha^{-1}$ from the $\varphi$-exponential construction, $\sin^2\theta_W$ from the geometric factor $(3-\varphi)/6$, and zero free parameters for the three SM gauge couplings. It does not close the OPEN infrared boundary condition on the exact CODATA $\alpha^{-1}(0)$; it only packages the RS-native product for scorecard use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.