friedmann_coeff
plain-language theorem explainer
Radiation-era Friedmann coefficient $8\pi^2/90$ that multiplies $G\,g_\star\,T^4$ to give $H^2$. Anyone assembling the Hubble rate at the electroweak temperature on the $\varphi$-ladder cites this constant. It is a pure definitional binding of the Stefan-Boltzmann prefactor for relativistic species; no proof obligations.
Claim. Define the radiation-era Friedmann coefficient as $\frac{8\pi^2}{90}$, so that the Hubble rate satisfies $H^2 = \frac{8\pi^2}{90}\, G\, g_\star\, T^4$ in the radiation-dominated era.
background
The module builds an RS-native scaffold for the electroweak phase transition on the $\varphi$-ladder. $T_{\mathrm{EW}}$ is identified with rung 51 (the $Z$-boson mass scale), and the radiation-era Friedmann equation is written with the full $T^4$ factor included.
In standard cosmology, $H^2 = (8\pi/3) G \rho_{\mathrm{rad}}$ with $\rho_{\mathrm{rad}} = (\pi^2/30) g_\star T^4$. Combining these yields the prefactor $8\pi^2/90$. In RS-native units $G = \varphi^5/\pi$, so the same coefficient appears as $H^2 = (8\pi^2/90)\cdot(\varphi^5/\pi)\cdot g_\star\cdot T^4 = (8\pi/90),\varphi^5, g_\star, T^4$.
Sibling constants in the module fix $g_\star^{\mathrm{EW}} = 106.75$ and $G_{\mathrm{RS}} = \varphi^5/\pi$; this coefficient is the remaining pure-number piece of that product.
proof idea
One-line definitional binding: the real constant is set equal to $8\pi^2/90$. No lemmas, tactics, or obligations. Downstream positivity is discharged separately by unfolding and positivity.
why it matters
This constant is the numerical spine of the radiation-era Hubble rate at $T_{\mathrm{EW}}$. It is multiplied into hubble_sq_at_ew together with RS-native $G$, $g_\star^{\mathrm{EW}}$, and $T_{\mathrm{EW}}^4$, and its positivity is recorded both as a standalone fact and as a field of the EWTransitionCert certificate structure (the washout-efficiency scaffold).
The module status is explicitly MODEL / scaffold: the resulting sphaleron-to-Hubble ratio is not fed into the Planck-matched $\eta_B = \varphi^{-44}(1-\varphi^{-8})^2$ expression. The coefficient itself is the classical Stefan-Boltzmann factor; what is RS-specific is the surrounding unit choice $G = \varphi^5/\pi$ (primer landmark) and the $\varphi$-ladder placement of $T_{\mathrm{EW}}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.