g_star_ew_matches_threshold_fn
plain-language theorem explainer
The fixed electroweak g★ = 106.75 is exactly the high-T value of the temperature-dependent SM step function g★(T) at T = 200 GeV. Cosmology and baryogenesis calculations that pin H(T_EW) to a constant DOF count can cite this to show the constant is a function evaluation, not an independent free parameter. The proof rewrites via the high-T threshold lemma and closes by rational arithmetic.
Claim. The electroweak effective relativistic degree-of-freedom count equals the high-temperature evaluation of the SM threshold function: $g_\star^{\mathrm{EW}} = g_\star(200\,\mathrm{GeV})$ as real numbers, where the right-hand side is the rational value $427/4 = 106.75$.
background
In the radiation era the Friedmann equation is $H^2 = (8\pi^2/90),G,g_\star,T^4$. The factor $g_\star$ counts relativistic SM degrees of freedom (bosons plus fermions with the $7/8$ thermal weight). At temperatures well above the electroweak scale every SM species is relativistic, giving the textbook value $106.75 = 427/4$.
This module places the electroweak transition on the $\varphi$-ladder: $T_{\mathrm{EW}} = \varphi^{51}$ (rung of the $Z$ mass, up to a unit prefactor). It builds $H(T_{\mathrm{EW}})$ and a sphaleron-to-Hubble scaffold in RS-native units with $G = \varphi^5/\pi$. The fixed constant used at $T_{\mathrm{EW}}$ is declared as $g_\star^{\mathrm{EW}} := 106.75$.
Upstream, GStarThresholds.g_star is the temperature-dependent step model (valid for $T \gtrsim 1,\mathrm{MeV}$, minimal-neutrino convention). Its high-T clause states that at $T = 200,\mathrm{GeV}$ one obtains exactly $427/4$. The baryon-asymmetry side module records the same $106.75$ as imported SM bookkeeping with RS-sourced gauge group and generation count, not a new RS prediction.
proof idea
One short tactic proof. Rewrite the right-hand side with the high-temperature evaluation lemma for the threshold function (which identifies $g_\star(200)$ with the rational $427/4$). Then norm_num unfolds the left-hand side definition $g_\star^{\mathrm{EW}} = 106.75$ and checks the real equality $106.75 = 427/4$.
why it matters
The module status is an honest RS-native scaffold for the electroweak transition and $H(T_{\mathrm{EW}})$, not a derivation of $\eta_B$. Pinning the constant DOF count to the threshold function prevents treating $106.75$ as a free-standing dial when assembling $H^2 \propto G,g_\star,T^4$ and the washout ratio $\Gamma_{\mathrm{sph}}/(H\cdot T)$.
No downstream theorem currently depends on this bridge (used-by is empty). It still closes the provenance loop advertised in the local docs: the fixed EW value is the high-T point of the same step function used elsewhere in the cosmology stack. It does not touch the forcing chain T0–T8, the RCL, or the $\alpha$ band; those live upstream of the $\varphi$-ladder and $G = \varphi^5/\pi$ already assumed here.
The open question left explicit by the module header remains: feeding a genuine Boltzmann-transport treatment rather than citing the separate Planck-matched $\eta_B = \varphi^{-44}(1-\varphi^{-8})^2$ expression, which carries neither $g_\star$ nor $\Gamma_{\mathrm{sph}}/H$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.