SphaleronRateCert
plain-language theorem explainer
Certificate bundling the RS sphaleron-rate claims: the prefactor equals 3/4 from Q₃ Hamiltonian-cycle combinatorics, both prefactor and weak coupling are positive, and the dimensionless rate equals that prefactor times α_W to the fifth and is positive. Cosmology and baryogenesis proofs cite it as the single provenance object for Γ_sph/T⁴. It is a pure structure; the inhabiting theorem wires five already-proved component facts.
Claim. A certificate asserting five facts: the sphaleron prefactor equals $3/4$; that prefactor is positive; the weak coupling $\alpha_W$ is positive; the dimensionless thermal rate $\Gamma_{\mathrm{sph}}/T^4$ is positive; and $\Gamma_{\mathrm{sph}}/T^4 = \kappa_{\mathrm{sph}}\,\alpha_W^5$.
background
Sphalerons are nonperturbative SU(2) configurations that violate baryon number. Above the electroweak transition the standard thermal rate is $\Gamma_{\mathrm{sph}}/T^4 = \kappa_{\mathrm{sph}},\alpha_W^5$, with $\kappa_{\mathrm{sph}}$ an $O(1)$ prefactor and $\alpha_W$ the weak coupling.
In this module $\kappa_{\mathrm{sph}}$ is fixed by Q₃ topology: a sphaleron path changes all three winding numbers at once, counted by Hamiltonian cycles on $K_4$ (the complete graph on the even sign-flip subgroup $(\mathbb{Z}/2\mathbb{Z})^2$). There are 3 such cycles, each with 4 edges, and $|\mathrm{even,sign,flips}|^2 = 16$, so $\kappa_{\mathrm{sph}} = 12/16 = 3/4$. Lattice estimates sit in $0.1$–$1.0$; the RS value $0.75$ lies inside that band.
The weak coupling enters as $\alpha_W = \alpha/\sin^2\theta_W$ (tree-level electroweak identity). The structure of the rate is RS-derived; the electromagnetic $\alpha$ input remains a boundary datum.
proof idea
No proof body: this is a structure definition whose five fields are the mathematical claims above. Downstream, the theorem sphaleron_rate_cert inhabits it by assigning kappa_sph_eq (equality to $3/4$), kappa_sph_pos, alpha_W_pos, sphaleron_rate_pos, and rfl for the rate formula (definitional unfolding of $\kappa_{\mathrm{sph}},\alpha_W^5$).
why it matters
Packages the entire sphaleron-rate provenance so baryogenesis can cite one object rather than five scattered lemmas. The parent certificate BaryonAsymmetryExactCert lists the sphaleron rate among the intermediaries (with $J_{CP}>0$ and the Sakharov conditions) needed for the exact $\eta_B$ chain: rung $44=4\times 11$, the identity $\varphi^{-44}\varphi^{45}=\varphi$, and $\eta_B,\varphi^{45}=\varphi$.
Within RS this is the cosmology-side use of the Q₃ / eight-tick cube topology (T7) and the weak coupling from the Standard Model layer. The honest provenance note matters: $\kappa_{\mathrm{sph}}$ is combinatorial and structural; $\alpha_W$ still carries the boundary electromagnetic $\alpha$. Status in-module is zero sorry and zero axiom once the certificate is inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.