ew_transition_cert
plain-language theorem explainer
Packages the electroweak transition scaffold into a single certificate: rung 51, g★ = 106.75, and positivity of T_EW, the Friedmann coefficient, G, H²(T_EW), the sphaleron-to-Hubble ratio, and the washout factor R/g★. Cosmology and baryogenesis workers cite it as the one-shot witness that the RS-native EW radiation-era quantities are well-defined and positive. The proof is a structure inhabitant built from rfl equalities and the module's positivity lemmas.
Claim. There exists a certificate asserting: the electroweak ladder rung equals $51$; the effective relativistic degrees of freedom satisfy $g_\star^{\mathrm{EW}} = 106.75$; and $T_{\mathrm{EW}} > 0$, the Friedmann prefactor $(8\pi/90)\varphi^5 > 0$, $G = \varphi^5/\pi > 0$, $H^2(T_{\mathrm{EW}}) > 0$, the sphaleron-to-Hubble ratio $> 0$, and the washout efficiency $R/g_\star > 0$.
background
This module places the electroweak phase transition on the φ-ladder in RS-native units. The Z mass sits at EW sector rung 51; the transition temperature is taken as $T_{\mathrm{EW}} = \varphi^{51}$ (the MeV unit prefactor drops out of dimensionless ratios). In the radiation era,
$$H^2 = \frac{8\pi}{3} G \rho_{\mathrm{rad}} = \frac{8\pi^2}{90} G, g_\star, T^4,$$
and with $G = \varphi^5/\pi$ this becomes $H^2 = (8\pi/90),\varphi^5, g_\star, T^4$. The module fixes $g_\star^{\mathrm{EW}} = 106.75$ and builds the sphaleron-to-Hubble ratio and the washout factor $R/g_\star$.
Per the module status tag, this is an RS-native-unit scaffold: it implements the full $T^4$ Friedmann combination but does not feed the washout ratio into the Planck-matched $\eta_B$ formula. The certificate structure simply bundles the rung identity, the $g_\star$ value, and the positivity of every intermediate quantity used downstream of those definitions.
proof idea
Term-mode structure inhabitant. The two equalities (ew_rung = 51, g_star_ew = 106.75) are discharged by rfl. The six positivity fields are filled by the corresponding lemmas already proved in the module: T_ew_pos, friedmann_coeff_pos, G_rs_pos (also available from Constants.GravitationalConstant), hubble_sq_at_ew_pos (product of the three positive factors times $T_{\mathrm{EW}}^4$), sphaleron_hubble_ratio_pos, and effective_washout_pos (quotient of the ratio by $g_\star > 0$). No new algebra is performed here.
why it matters
Closes Part 5 of the EW phase-transition module by packaging every well-definedness obligation into one named certificate. In the Recognition framework this sits under the cosmology scaffold that uses $G = \varphi^5/\pi$ (RS-native units from the forcing chain) and the φ-ladder mass/temperature placement at rung 51. The certificate makes the positive-definite radiation-era EW quantities available as a single hypothesis for any future Boltzmann-transport or genuine washout calculation; it does not itself derive $\eta_B$. No downstream consumers are wired yet (used_by is empty), so its present role is internal module closure and auditability after the 2026-06-25 external review that required the $T^4$ factor and honest scope tags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.