hubble_sq_at_ew_pos
plain-language theorem explainer
The squared Hubble rate at the electroweak temperature is strictly positive in RS-native units. Cosmologists building the sphaleron-to-Hubble washout ratio cite it to justify taking a real square root for H(T_EW). The proof is a four-factor positivity chase after unfolding the radiation-era Friedmann product.
Claim. In RS-native units, $H^2(T_{\mathrm{EW}}) = c_{\mathrm{F}} \, G_{\mathrm{RS}} \, g_\star^{\mathrm{EW}} \, T_{\mathrm{EW}}^4$ satisfies $H^2(T_{\mathrm{EW}}) > 0$, where $c_{\mathrm{F}} = 8\pi/90$ is the radiation-era Friedmann coefficient, $G_{\mathrm{RS}} = \varphi^5/\pi$, $g_\star^{\mathrm{EW}} = 106.75$, and $T_{\mathrm{EW}} = \varphi^{51}$.
background
This module places the electroweak phase transition on the φ-ladder. The Z-boson mass sits at EW rung 51; the transition temperature is taken as $T_{\mathrm{EW}} = \varphi^{51}$ in RS-native units (the MeV prefactor is a unit choice and drops out of dimensionless ratios). Status is MODEL scaffold: radiation-era Friedmann quantities only, not a full Boltzmann transport of baryon asymmetry.
In the radiation era the Friedmann equation is $H^2 = (8\pi/3) G \rho_{\mathrm{rad}}$ with $\rho_{\mathrm{rad}} = (\pi^2/30) g_\star T^4$. With $G = \varphi^5/\pi$ this collapses to $H^2 = (8\pi/90),\varphi^5, g_\star, T^4$. The definition hubble_sq_at_ew packages exactly that product: friedmann coefficient times $G_{\mathrm{RS}}$ times $g_\star^{\mathrm{EW}}$ times $T_{\mathrm{EW}}^4$ (the $T^4$ factor is explicit after the 2026-06-25 review fix).
Upstream positivity is already on the shelf: $G_{\mathrm{RS}} > 0$ from $\varphi^5/\pi$, the Friedmann coefficient is positive by positivity, $g_\star^{\mathrm{EW}} = 106.75 > 0$ by norm_num, and $T_{\mathrm{EW}} = \varphi^{51} > 0$.
proof idea
Term-mode positivity after one unfold. Expand $H^2(T_{\mathrm{EW}})$ into the four-factor product, then chain mul_pos three times on friedmann_coeff_pos, G_rs_pos, and g_star_ew_pos, and finish with pow_pos T_ew_pos 4 for the temperature power. No algebraic cancellation or case split; every factor is independently positive.
why it matters
Without $H^2 > 0$ one cannot form the physical Hubble rate $H = \sqrt{H^2}$ that enters the sphaleron-to-Hubble ratio $R = (\Gamma_{\mathrm{sph}}/T^4), T^3 / H$. Downstream, sphaleron_hubble_ratio_pos invokes this lemma via Real.sqrt_pos.mpr to prove $R > 0$, which is the washout-efficiency scaffold of Part 3–4. The certificate ew_transition_cert packages the same positivity stack for the EW transition bundle.
In the broader RS picture this sits in the cosmology layer that uses $G = \varphi^5/\pi$ (primer constants) and the φ-ladder mass/temperature placement. It does not yet close the gap to the Planck-matched $\eta_B = \varphi^{-44}(1-\varphi^{-8})^2$ expression; the module doc is explicit that these quantities are a separate positive-definite scaffold for a future Boltzmann treatment, not the origin of the $\eta_B$ prefactor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.