friedmann_coeff_pos

This module builds an RS-native scaffold for the electroweak phase transition on the $\varphi$-ladder: $T_{\mathrm{EW}}=\varphi^{51}$, a fixed $g_\star$ at that scale, and the radiation-era Hubble rate. In the radiation-dominated era the Friedmann equation is

$$H^2 = \frac{8\pi}{3} G \rho_{\mathrm{rad}} = \frac{8\pi}{3} G \cdot \frac{\pi^2}{30}, g_\star T^4,$$

which rearranges to $H^2 = C, G, g_\star T^4$ with coefficient $C = 8\pi^2/90$ (Stefan–Boltzmann for relativistic species). The local definition friedmann_coeff is exactly that constant.

In RS-native units one further substitutes $G=\varphi^5/\pi$, so $H^2=(8\pi/90),\varphi^5, g_\star T^4$. Positivity of $C$ is the first algebraic gate before multiplying by the positive factors $G$, $g_\star$, and $T^4$.

Unfold the definition of the coefficient to the concrete real $8\pi^2/90$. Mathlib's positivity tactic then discharges $0 < 8\pi^2/90$ from the known positivity of $\pi$ and of squares of nonzero reals, together with division by a positive denominator. No external RS lemmas are required.

This is a tiny but mandatory positivity lemma in the EW-transition certificate chain. Downstream, hubble_sq_at_ew_pos multiplies it with $G_{\mathrm{RS}}>0$, $g_\star^{\mathrm{EW}}>0$, and $T_{\mathrm{EW}}^4>0$ to conclude $H^2(T_{\mathrm{EW}})>0$. The bundle certificate ew_transition_cert records the same fact as the field friedmann_positive, so any consumer of the EW scaffold can assume the radiation-era prefactor is positive without re-proving it.

Within Recognition Science this sits in the cosmology layer that uses the RS-native $G=\varphi^5/\pi$ (primer constants) inside a radiation-era Friedmann combination. It does not touch the forcing chain T0–T8, the RCL, or the $\eta_B$ prefactor; the module doc explicitly scopes it as a positive-definite scaffold for a future Boltzmann-transport treatment, not as the origin of baryon asymmetry numerics.