EWTransitionCert
plain-language theorem explainer
Certificate bundling the electroweak φ-ladder rung, SM g★ at the EW scale, and positivity of the radiation-era Hubble ingredients and washout scaffold. Cosmologists citing the RS-native EW transition setup use it as a single witness that the numerical anchors and sign constraints hold. Instantiation is by reflexivity on the two equalities plus the existing positivity lemmas.
Claim. A certificate record asserting: the electroweak ladder rung equals $51$; the effective relativistic degrees of freedom at the EW scale equal $106.75$; and the RS-native EW temperature $T_{\mathrm{EW}}=\varphi^{51}$, the Friedmann coefficient $8\pi^2/90$, Newton's constant $G=\varphi^5/\pi$, the squared Hubble rate $H^2(T_{\mathrm{EW}})$, the sphaleron-to-Hubble ratio, and the washout factor $R/g_\star$ are all strictly positive.
background
This module is an RS-native-unit scaffold for the electroweak phase transition on the φ-ladder. The Z-boson mass sits at EW-sector rung 51, so the transition temperature is taken as $T_{\mathrm{EW}}=\varphi^{51}$ (sector unit prefactors absorbed into the unit choice). In the radiation era the Friedmann equation is $H^2=(8\pi^2/90),G,g_\star,T^4$, with $G=\varphi^5/\pi$ in RS-native units and $g_\star=106.75$ the standard high-$T$ SM value.
The sphaleron-to-Hubble ratio and the derived washout factor (that ratio divided by $g_\star$) are positive-definite bookkeeping quantities only. Per the module status tag and the 2026-06-25 review, they are not fed into the Planck-matched baryon asymmetry $\eta_B=\varphi^{-44}(1-\varphi^{-8})^2$, which contains neither $g_\star$ nor $\Gamma_{\mathrm{sph}}/H$.
Sibling positivity lemmas (T_ew_pos, friedmann_coeff_pos, G_rs_pos, and the corresponding Hubble, ratio, and washout facts) discharge the sign fields of the certificate.
proof idea
No proof body: this is a structure (Prop-valued fields). Downstream, ew_transition_cert builds an inhabitant by rfl on the two numerical equalities (rung $51$, $g_\star=106.75$) and by citing the existing positivity theorems for $T_{\mathrm{EW}}$, the Friedmann coefficient, $G$, $H^2$ at EW, the sphaleron-Hubble ratio, and effective washout.
why it matters
Gives a single typed witness that the EW-scale anchors and radiation-era sign constraints are in place before any further cosmology lemmas quote them. The sole consumer is ew_transition_cert, which packages the scaffold for downstream use.
In the Recognition framework this sits at the cosmology layer above the forcing chain: $G=\varphi^5/\pi$ is the RS-native gravitational constant from the primer, and the EW rung $51$ is the φ-ladder placement of the Z scale. It does not close the open Boltzmann-transport link from washout to $\eta_B$; the module explicitly flags that connection as open and forbids citing the washout factor as the origin of the $\eta_B$ prefactor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.