effective_washout
plain-language theorem explainer
Defines the electroweak washout efficiency as the dimensionless sphaleron-to-Hubble ratio divided by the effective relativistic degrees of freedom at the EW scale. Cosmologists and baryogenesis workers cite it as the combination R/g★ that multiplies the CP asymmetry in the standard η_B scaling. It is a one-line quotient of two already-defined positive reals, not a derived identity.
Claim. The effective washout factor is the real number $R/g_\star$, where $R=\Gamma_{\mathrm{sph}}/(H\,T)$ is the dimensionless sphaleron-to-Hubble ratio at the electroweak temperature and $g_\star=106.75$ is the high-$T$ Standard Model effective degrees of freedom.
background
The module builds an RS-native scaffold for the electroweak phase transition on the φ-ladder. The transition temperature is taken as $T_{\mathrm{EW}}=\varphi^{51}$ (Z-boson rung), and the radiation-era Hubble rate follows from the Friedmann equation $H^2=(8\pi^2/90),G,g_\star,T^4$ with $G=\varphi^5/\pi$ in RS units.
Upstream, $g_\star$ at the EW scale is fixed at the standard high-$T$ SM value $106.75$ (gauge group and generation count RS-derived; matter representations and the $7/8$ thermal factor imported). The sphaleron-Hubble ratio is $R=(\Gamma_{\mathrm{sph}}/T^4),T^3/\sqrt{H^2}$, with the $T^3$ and $T^4$ factors now explicit after the 2026-06-25 review fix.
In textbook electroweak baryogenesis one writes $\eta_B\propto(\varepsilon_{\mathrm{CP}}/g_\star)\times\min(1,R)$. The quantity defined here is exactly the combination $R/g_\star$.
proof idea
Pure definition: the real is the quotient of the already-constructed sphaleron-Hubble ratio by $g_\star$ at the EW scale. No tactics, no lemmas, no algebraic reduction beyond division of two positive reals.
why it matters
Feeds the positivity lemma (the quotient is positive because both factors are) and the EW transition certificate structure, which packages rung 51, $g_\star=106.75$, positivity of $T_{\mathrm{EW}}$, the Friedmann coefficient, and $G$. It also appears among the intermediaries listed by the complete baryon-asymmetry exact certificate.
Framework role is deliberately narrow. The module status tag is MODEL (RS-native-unit scaffold). The Planck-matched expression $\eta_B=\varphi^{-44}(1-\varphi^{-8})^2$ contains neither $g_\star$ nor $\Gamma_{\mathrm{sph}}/H$; this washout factor is not its origin. A genuine link would require Boltzmann transport through the transition, which remains open. Cite only as the positive-definite $R/g_\star$ scaffold, not as a derivation of the observed baryon asymmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.