T_ew_pos
plain-language theorem explainer
The RS-native electroweak temperature on the φ-ladder is strictly positive. Cosmology proofs that assemble H²(T_EW), the sphaleron-to-Hubble ratio, or the EW transition certificate cite this lemma as the positivity gate. The argument is a one-line term application of positivity of natural powers of φ.
Claim. Let $T_{\mathrm{EW}} = \varphi^{51}$ be the RS-native electroweak temperature on the $\varphi$-ladder. Then $0 < T_{\mathrm{EW}}$.
background
The module places the electroweak phase transition on the φ-ladder in RS-native units. The Z-boson mass sits at EW-sector rung 51; the transition temperature is identified with that rung, so $T_{\mathrm{EW}} = \varphi^{51}$. Sector unit prefactors (the $2/10^6,\mathrm{MeV}$ conversion) are absorbed into the unit choice; only the φ-power structure enters the dimensionless ratios built downstream.
In the radiation era the Friedmann equation is written $H^2 = (8\pi^2/90),G,g_\star,T^4$ with $G = \varphi^5/\pi$. Positivity of $T_{\mathrm{EW}}$ is the first gate before $T^4$, $H^2$, and $\Gamma_{\mathrm{sph}}/(H,T)$ can be shown positive. The golden ratio $\varphi > 1$ (hence $\varphi > 0$) is a fixed constant of the Recognition framework (T6 self-similar fixed point).
proof idea
One-line term proof. Unfold $T_{\mathrm{EW}} = \varphi^{51}$ and apply pow_pos to the known fact $\varphi > 0$ at exponent 51. No case splits, no arithmetic beyond the power-positivity lemma.
why it matters
This is the positivity hinge for the EW scaffold. Downstream it is wired into three parents: the EW transition certificate (field t_ew_positive), positivity of $H^2$ at the EW scale (via pow_pos T_ew_pos 4 inside the $T^4$ factor), and positivity of the sphaleron-to-Hubble ratio (via $T_{\mathrm{EW}}^3$ in the numerator and $\sqrt{H^2}$ in the denominator).
Within the Recognition chain the rung-51 placement ties the EW scale to the φ-ladder mass formula (yardstick $\cdot,\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). The module is explicitly scoped as a MODEL scaffold: it builds a positive-definite washout ratio but does not feed that ratio into the Planck-matched $\eta_B = \varphi^{-44}(1-\varphi^{-8})^2$ expression. Closing a genuine Boltzmann-transport link remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.