effective_washout_pos
plain-language theorem explainer
The electroweak washout efficiency factor R/g★ is strictly positive. Cosmologists citing the EW-transition scaffold or the baryon-asymmetry certificate use this to keep denominators and certificate fields well-defined. The proof is a one-line positivity of a quotient: both the sphaleron-to-Hubble ratio and g★_EW are already known positive.
Claim. The effective washout efficiency $R/g_\star$ at the electroweak scale is strictly positive: $0 < \Gamma_{\mathrm{sph}}/(H\,T)\,/\,g_\star^{\mathrm{EW}}$.
background
This module places 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 Friedmann equation is written in RS-native units with $G=\varphi^5/\pi$, so $H^2=(8\pi/90),\varphi^5,g_\star,T^4$.
The sphaleron-to-Hubble ratio $R=\Gamma_{\mathrm{sph}}/(H T)$ is assembled upstream; sphaleron_hubble_ratio_pos records that both the cubic temperature factor in the rate and $\sqrt{H^2}$ are positive. The effective degrees of freedom at the EW scale are the fixed high-$T$ value $g_\star^{\mathrm{EW}}=106.75$, already shown positive by g_star_ew_pos.
The washout efficiency factor is the quotient $R/g_\star$. In standard EW baryogenesis sketches one writes $\eta_B\propto(\varepsilon_{\mathrm{CP}}/g_\star)\min(1,R)$; this definition isolates the combination $R/g_\star$ as a positive-definite scaffold, not a full Boltzmann washout integral.
proof idea
Term-mode one-liner. Unfold the definition of the washout factor to the quotient sphaleron_hubble_ratio / g_star_ew, then apply div_pos to the two upstream positivity lemmas: sphaleron_hubble_ratio_pos (numerator) and g_star_ew_pos (denominator). No further algebraic work.
why it matters
Feeds the local certificate ew_transition_cert, which packages positivity of the EW scale, $g_\star$, Friedmann coefficient, and $G$ for the module. Also sits on the depends-on edge into baryon_asymmetry_exact_cert in BaryonAsymmetryExact, whose doc-comment ties $\eta_B$ to φ-rung $-44$ and the Q₃ cube geometry (with sphaleron input carrying the α boundary datum).
Within the Recognition framework this is scaffolding under the cosmology domain: it keeps the washout combination positive so certificate fields type-check, while the module doc explicitly warns that the Planck-matched $\eta_B=\varphi^{-44}(1-\varphi^{-8})^2$ expression does not consume $g_\star$ or $\Gamma_{\mathrm{sph}}/H$. The result therefore closes a positivity obligation without claiming a thermal transport derivation of the observed baryon asymmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.