g_star
plain-language theorem explainer
Defines the temperature-dependent effective relativistic degrees of freedom g_*(T) under the minimal-SM neutrino convention (three left-handed neutrinos plus antineutrinos). Cosmology modules cite it for epoch-dependent entropy and expansion bookkeeping above about 1 MeV. The body is a one-line specialization of the parameterized sum over active species.
Claim. For rational temperature $T$, $g_*(T)$ is the sum of relativistic degree-of-freedom weights of all Standard Model species still active at $T$, using the minimal neutrino sector (six Weyl degrees of freedom) and an instantaneous mass-threshold step model.
background
In early-universe thermodynamics the expansion rate and entropy density track an effective count $g_*(T)$ of relativistic degrees of freedom. The standard leading model is a step function: each species contributes its full thermal weight while $T$ exceeds its mass threshold and drops out below it; at the QCD crossover the strong sector switches from quark–gluon plasma content to pions.
This module implements that bookkeeping over exact rationals. Species records (photons, neutrinos, quarks, leptons, gauge bosons, Higgs) carry name, mass threshold, degree count, and a fermionic flag. The helper g_starWith sums the per-species weights of those still active at $T$. The neutrino record used here is the minimal-SM convention: three generations of left-handed $\nu$ plus right-handed $\bar\nu$, totaling six degrees of freedom.
The module answers an external review point that RS previously fixed a single high-$T$ number without a $T$-dependent function. Mass thresholds are imported PDG-rounded rationals used only for ordering; particle content matches the SM relativistic-DOF assembly (gauge group and generation count RS-sourced; representations and the $7/8$ fermionic weight imported).
proof idea
One-line definitional wrapper: specialize the parameterized sum g_starWith to the fixed minimal-neutrino species record. No tactics or lemmas; evaluation theorems later in the file discharge concrete rational values (e.g. $T=200,\mathrm{GeV}$ yields $427/4$).
why it matters
Supplies the temperature-dependent $g_(T)$ that cosmology needs once a single high-$T$ constant is no longer enough. Downstream, the electroweak module proves the fixed $g_{,\mathrm{EW}}=106.75$ equals this function at $T=200,\mathrm{GeV}$, so the constant is a function value rather than a free-standing import. Baryon-asymmetry scaffolding divides the structural Jarlskog invariant by $g_*$ for the sign theorem $\eta_B>0$ and a weak smallness bound. The GStar derivation certificate also consumes it.
Within RS this is model-layer SM bookkeeping (instantaneous thresholds, minimal neutrinos), not a forcing-chain prediction like T5–T8. It closes the gap between the single high-$T$ assembly in RelativisticDOF and epoch-dependent cosmology while staying honest about omitted Boltzmann tails and neutrino reheating.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.