sphaleron_rate_structural
plain-language theorem explainer
The dimensionless sphaleron rate equals the combinatorial prefactor κ_sph times the fifth power of the weak coupling. Cosmologists computing baryon-number violation above the electroweak transition cite this identity as the RS rate formula. Proof is reflexivity: the rate is defined to be exactly that product.
Claim. The dimensionless sphaleron rate equals $\kappa_{\mathrm{sph}}\,\alpha_W^5$, i.e. $\Gamma_{\mathrm{sph}}/T^4 = \kappa_{\mathrm{sph}}\,\alpha_W^5$, where $\kappa_{\mathrm{sph}}$ is the $Q_3$-topology prefactor and $\alpha_W$ is the weak coupling.
background
Sphalerons are nonperturbative SU(2) configurations that violate baryon number. Above the electroweak phase transition the thermal rate per unit volume is written $\Gamma_{\mathrm{sph}}/T^4 = \kappa_{\mathrm{sph}},\alpha_W^5$. In this module $\alpha_W$ is imported from the weak-coupling construction; $\kappa_{\mathrm{sph}}$ is fixed by $Q_3$ topology.
Concretely, $\kappa_{\mathrm{sph}}$ counts Hamiltonian cycles on $K_4$ (the complete graph on the four even sign-flip vertices of the cube): three cycles, four edges each, normalized by the square of the even-sign-flip count, yielding $(3\times 4)/4^2 = 3/4$. The dimensionless rate is then defined as the product of that prefactor with $\alpha_W^5$.
The surrounding certificate notes that the combinatorial skeleton is RS-derived while the numerical $\alpha$ input that feeds $\alpha_W$ remains a boundary datum.
proof idea
One-line term proof by rfl. The dimensionless rate is defined to be exactly $\kappa_{\mathrm{sph}}\cdot\alpha_W^5$, so the equality is definitional and needs no further lemmas.
why it matters
Pins the structural form of the RS sphaleron rate: $\Gamma_{\mathrm{sph}}/T^4 = \kappa_{\mathrm{sph}},\alpha_W^5$ with $\kappa_{\mathrm{sph}}=3/4$ from $Q_3$ Hamiltonian cycles. Lattice estimates place $\kappa_{\mathrm{sph}}$ in roughly $0.1$–$1$; the RS value $3/4$ sits inside that band. The companion positivity result uses the same product; the provenance note records that the $\alpha$ factor feeding $\alpha_W$ is a boundary datum, not an internal derivation. No downstream consumers are wired yet; the declaration closes the structural half of the rate formula inside the cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.