IndisputableMonolith.StandardModel.WeakCoupling
Defines the weak fine-structure constant α_W = α / sin²θ_W from the tree-level identity α_EM = α_W sin²θ_W. Packages positivity, α_W > α, α_W > 2α, and 0 < sin²θ_W < 1/2, plus a WeakCouplingCert bundle. Cosmology imports (sphaleron rate, baryon asymmetry) cite it for the α_W⁵ factor. Arguments are short algebraic inequalities from the RS α band and angle bounds.
claimThe module defines the weak coupling $\alpha_W := \alpha / \sin^2\theta_W$ from the tree-level electroweak identity $\alpha_{\mathrm{EM}} = \alpha_W \sin^2\theta_W$, and records $\alpha_W > 0$, $\alpha_W > \alpha$, $\alpha_W > 2\alpha$, and $0 < \sin^2\theta_W < 1/2$, with a certificate packing those facts.
background
At tree level in the electroweak theory, the electromagnetic fine-structure constant factors as $\alpha = \alpha_W \sin^2\theta_W$, so the weak coupling is $\alpha_W = \alpha / \sin^2\theta_W$. Recognition Science supplies $\alpha$ in RS-native units via Constants and Constants.Alpha (predicted $\alpha^{-1}$ inside roughly $(137.030, 137.039)$). ElectroweakMasses places the $Z$ on the $\varphi$-ladder (rung 1 in the electroweak sector) and is imported for sector context, not for the coupling algebra itself.
Sibling objects in the module include the expanded form of $\alpha_W$, positivity lemmas for $\alpha$ and $\sin^2\theta_W$, the half-bound $\sin^2\theta_W < 1/2$, the comparison $\alpha_W > 2\alpha$, and a WeakCouplingCert / weak_coupling_cert pair that bundles the certified inequalities for downstream use.
proof idea
Definition-and-inequality module, not a deep derivation. $\alpha_W$ is introduced by the quotient $\alpha/\sin^2\theta_W$. Positivity is multiplication of $\alpha > 0$ by the reciprocal of $\sin^2\theta_W > 0$. The comparisons $\alpha_W > \alpha$ and $\alpha_W > 2\alpha$ are rearrangements of $\sin^2\theta_W < 1$ and $\sin^2\theta_W < 1/2$. The certificate is a structure packing those proved facts so cosmology modules can import a single object rather than re-prove the bounds.
why it matters in Recognition Science
SphaleronRate imports this module because the nonperturbative baryon-violating rate is written $\Gamma_{\mathrm{sph}}/T^4 = \kappa_{\mathrm{sph}}\cdot\alpha_W^5$; without a formal $\alpha_W$ and positivity/size lemmas, that power cannot sit in Lean. BaryonAsymmetryExact likewise imports it while closing $\eta_B$ on $\varphi$-rung $-44$ and the balance $\eta_B\times\varphi^{45}=\varphi$. The module is the bridge from the RS $\alpha$ prediction (and electroweak mass sector) into early-universe weak-rate phenomenology used in the baryogenesis chain.
scope and limits
- Does not derive sin²θ_W from RS first principles; angle bounds are inputs.
- Does not include running couplings or loop-level electroweak corrections.
- Does not fix a unique numerical α_W beyond structural inequalities.
- Does not treat the SU(2) coupling g except through the α_W fine-structure form.
- Does not prove sphaleron or baryon-asymmetry formulas; those live downstream.