sphaleron_rate_pos
plain-language theorem explainer
The dimensionless thermal sphaleron rate Γ_sph/T⁴ is strictly positive. Cosmology proofs that need a live baryon-number-violating channel above the electroweak transition cite this fact. The argument is a one-line product of two positivity lemmas: the RS combinatorial prefactor κ_sph = 3/4 and the fifth power of the weak coupling α_W.
Claim. The dimensionless sphaleron rate $\Gamma_{\mathrm{sph}}/T^4 = \kappa_{\mathrm{sph}}\,\alpha_W^5$ satisfies $0 < \Gamma_{\mathrm{sph}}/T^4$, where $\kappa_{\mathrm{sph}} = 3/4$ is the RS combinatorial prefactor and $\alpha_W > 0$ is the weak fine-structure coupling.
background
Sphalerons are nonperturbative SU(2) gauge configurations that violate baryon number. Above the electroweak phase transition their thermal rate per unit volume is written $\Gamma_{\mathrm{sph}}/T^4 = \kappa_{\mathrm{sph}},\alpha_W^5$. In this module $\alpha_W$ is the weak coupling imported from the Standard Model layer, and $\kappa_{\mathrm{sph}}$ is fixed by Q₃ topology rather than left as a free O(1) lattice parameter.
The RS derivation counts Hamiltonian cycles on the complete graph $K_4$ through the even sign-flip subgroup $(\mathbb{Z}/2\mathbb{Z})^2$: three distinct 4-cycles, each with four edges, normalized by the squared order of that subgroup, yielding $\kappa_{\mathrm{sph}} = 12/16 = 3/4$. The sibling lemma kappa_sph_pos records $0 < 3/4$ by rewriting to the closed form and evaluating numerically. The dimensionless rate is then the product definition $\kappa_{\mathrm{sph}}\cdot\alpha_W^5$.
proof idea
Unfold the definition of the dimensionless rate to the product $\kappa_{\mathrm{sph}}\cdot\alpha_W^5$. Apply the real-multiplication positivity lemma to the pair of factors: the already-proved $0 < \kappa_{\mathrm{sph}}$ and $0 < \alpha_W^5$, the latter from $0 < \alpha_W$ raised to the fifth power. No further algebraic identities are required.
why it matters
Positivity of $\Gamma_{\mathrm{sph}}/T^4$ is a structural gate for electroweak baryogenesis in the RS cosmology stack. It is packaged into the local certificate sphaleron_rate_cert (alongside the Q₃ origin of $\kappa_{\mathrm{sph}}$ and the rate formula) and is consumed by sphaleron_hubble_ratio_pos, which shows the sphaleron-to-Hubble ratio at the electroweak temperature is positive. Downstream, the baryon-asymmetry exact certificate uses the sphaleron-rate input (with the $\alpha$ boundary datum) so that the baryon-to-photon ratio sits on the $\varphi$-rung $-44$ with the exact balance $\eta_B\cdot\varphi^{45}=\varphi$. The result is unconditional positivity only; it does not by itself fix the numerical size of washout or the freeze-out temperature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.