alphaInv_MZ
plain-language theorem explainer
Fixes the inverse fine-structure constant at the Z pole to the PDG working value 128.9. Mass and electroweak consistency arguments cite it when converting a zero-momentum tree-level Higgs VEV into a physical-scale VEV. The body is a bare real constant, not a derived theorem.
Claim. Define the inverse fine-structure constant at the $Z$ pole by $\alpha^{-1}(M_Z) := 128.9$ (PDG conventional value).
background
The module VEVConsistency treats the Higgs vacuum expectation value as determined rather than free. The tree-level electroweak identity is $v^2 = m_Z^2 \cdot \sin^2\theta_W \cdot \cos^2\theta_W \cdot \alpha^{-1}/\pi$, with $m_Z$ from ElectroweakMasses, $\sin^2\theta_W = (3-\varphi)/6$ from WeinbergAngle, and the low-energy $\alpha^{-1}$ band from AlphaBounds.
At vanishing momentum that formula yields $v_{\mathrm{tree}}\approx 253,\mathrm{GeV}$, about 2.8% above the PDG VEV. The mismatch is attributed to QED vacuum-polarization running from $\alpha(0)$ to $\alpha(M_Z)$. The present constant supplies the high-scale endpoint of that running ratio.
In RS-native units the low-energy inverse coupling sits in $(137.030,137.039)$; the Z-pole value is the conventional PDG anchor used to form the dimensionless correction factor.
proof idea
Definitional constant: the real number 128.9 is assigned directly. No lemmas, tactics, or algebraic reduction are involved.
why it matters
Feeds the local running correction running_ratio $= \alpha^{-1}(M_Z)/\alpha^{-1}(0)$ and the interval theorem running_ratio_bounds that places that ratio in $(0.940,0.942)$. Those objects close the P5a partial story: multiplying the tree VEV by $\sqrt{128.9/137.036}\approx 0.970$ produces $v_{\mathrm{physical}}\approx 245.5,\mathrm{GeV}$, within $0.3%$ of the PDG $246.22,\mathrm{GeV}$.
In the broader Recognition chain this is bookkeeping, not a forcing step: $\alpha$ itself is constrained by the RS alpha band, while the Z-pole number is an external PDG input that converts the zero-momentum formula into a physical-scale check. It does not touch T5–T8, the RCL, or the mass ladder rungs; it only calibrates the electroweak VEV consistency certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.