g_star_high
plain-language theorem explainer
At T = 200 GeV every Standard Model species is relativistic, so the threshold step-function g_★(T) evaluates exactly to 427/4 = 106.75. Cosmology modules that need the high-T SM DOF count (EW transition, baryon asymmetry) cite this equality to replace a free-standing constant by a function value. The proof is a one-line native_decide on exact rational arithmetic.
Claim. At temperature $T = 200\,\mathrm{GeV}$, the temperature-dependent relativistic degree-of-freedom count (minimal-neutrino SM convention, instantaneous mass thresholds) equals $427/4 = 106.75$.
background
The module implements the standard instantaneous-threshold model of $g_\star(T)$: each SM species contributes its full relativistic DOF while $T$ exceeds its mass, and drops out below it; the QCD switch at $T_{\mathrm{QCD}}\approx 0.15,\mathrm{GeV}$ replaces quark–gluon plasma content by pions. All sums are exact over $\mathbb{Q}$. Valid domain is $T\gtrsim 1,\mathrm{MeV}$ (above neutrino decoupling).
The local definition is $g_\star(T) := g_{\star\mathrm{With}}(\nu_{\mathrm{minimal}}, T)$. Particle content and the $7/8$ fermionic weight are imported from StandardModel.RelativisticDOF (gauge group and generation count RS-derived; representations and neutrino convention imported). Mass thresholds are PDG-rounded rationals used only for ordering, so rounding cannot change the step counts.
At $T = 200,\mathrm{GeV}$ every listed species (photons, gluons, $W/Z$, Higgs, three generations of quarks and charged leptons, and three left-handed neutrinos) sits above threshold, recovering the textbook high-T value $106.75$.
proof idea
One-line tactic proof: native_decide. Lean evaluates the closed rational expression for $g_\star(200)$ by unfolding the species sum and the threshold predicates, then checks equality with $427/4$ by machine arithmetic on $\mathbb{Q}$. No lemmas are invoked beyond definitional reduction.
why it matters
Closes the external-review gap that "RS fixes one number" for $g_\star$: the old constant $106.75$ is now the high-$T$ value of an explicit function. Downstream, g_star_high_matches_derived rewrites $((g_\star,200:\mathbb{Q}):\mathbb{R})$ into StandardModel.RelativisticDOF.g_star_derived, and g_star_ew_matches_threshold_fn identifies the EW-epoch constant $g_{\star,\mathrm{EW}}$ with the same evaluation. Both parents treat the constant as a function value rather than a free parameter, which is required before Hubble-rate and baryon-asymmetry calculations at $T_{\mathrm{EW}}$ can claim a single consistent DOF bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.