g_star_ew_pos
plain-language theorem explainer
The electroweak-scale relativistic degree count equals 106.75 and is strictly positive. Cosmology proofs that assemble H²(T_EW) or the sphaleron washout ratio cite this to keep every factor in the radiation-era product positive. The proof is a one-line numeric check after unfolding the constant definition.
Claim. The effective number of relativistic degrees of freedom at the electroweak scale satisfies $0 < g_\star^{\mathrm{EW}}$, where $g_\star^{\mathrm{EW}} = 106.75$ is the standard high-temperature Standard Model value.
background
This module builds an RS-native scaffold for the electroweak phase transition on the φ-ladder. T_EW is identified with rung 51 (the Z-boson mass scale), and the radiation-era Friedmann equation is written H² = (8π/90)·φ⁵·g★·T⁴ in RS units with G = φ⁵/π.
The constant g★_EW is the fixed high-T SM bookkeeping value 106.75 (bosons 28, fermions 90 with the 7/8 weight, minimal-neutrino convention). Upstream, the same number appears as the plain SM constant in the baryon-asymmetry derivation and as the T = 200 GeV evaluation 427/4 of the temperature-dependent step function g_star(T). The gauge group and generation count are RS-sourced; the matter representations and thermal weights are imported SM content, not an independent RS prediction.
proof idea
Unfold the definition g_star_ew := 106.75 and discharge 0 < 106.75 by norm_num. No lemmas beyond the definitional equality are required; the tactic closes the inequality by exact rational arithmetic.
why it matters
Positivity of g★_EW is a leaf in the positivity chain for the radiation-era Hubble rate and the washout ratio. Downstream, hubble_sq_at_ew_pos multiplies friedmann_coeff_pos, G_rs_pos, this fact, and T_ew^4 > 0 to obtain H²(T_EW) > 0. Separately, effective_washout_pos divides the sphaleron-to-Hubble ratio by g★_EW and needs the denominator positive.
Within the Recognition scaffold this is bookkeeping, not a forcing-chain step: it keeps the EW washout construction well-defined so a future Boltzmann-transport treatment can sit on a positive-definite base. The module status tag is explicit that these quantities do not feed the Planck-matched η_B = φ⁻⁴⁴·(1−φ⁻⁸)² prefactor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.