g_starWith
plain-language theorem explainer
Parameterized temperature-dependent relativistic DOF count with the neutrino sector supplied as an explicit thermal species. Cosmologists comparing minimal-SM versus thermalized Dirac neutrinos cite this. It sums energy-density weights of every species still active at T under the instantaneous-threshold step model. The body is a one-line list map-and-sum over the active species table.
Claim. For a neutrino-sector species $\nu$ and temperature $T$ (GeV), $g_{\star}(\nu,T)$ equals the sum of energy-density weights of all thermal species that remain relativistic and populated at $T$, with $\nu$ fixed as the neutrino content.
background
This module answers an external review gap: RS previously fixed a single high-T $g_{\star}$ and did not expose a temperature-dependent step function, threshold decoupling, or epoch-dependent particle content. The model is the standard instantaneous-threshold approximation over adopted SM content, with exact rational arithmetic, valid for $T \gtrsim 1$ MeV.
A thermal species carries a name, mass threshold (GeV, PDG-rounded rational; only order relative to $T$ matters), internal DOF count, and a fermion flag. The weight of one species is its DOF, times $7/8$ if fermionic (spin-statistics sign RS-derived; the integral value $7/8$ imported). The active list at $T$ always includes the photon and the supplied neutrino species, plus electroweak species lighter than $T$, and either QGP content above $T_{\mathrm{QCD}}$ or hadrons lighter than $T$ below it.
The constant high-T SM value $g_{\star}=106.75$ (bosons 28, fermions 90 with $7/8$, minimal neutrinos) is the $T > T_{\mathrm{EW}}$ specialization assembled in StandardModel.RelativisticDOF; this definition is the temperature-dependent, neutrino-parameterized lift of that bookkeeping.
proof idea
Pure definition, not a proved theorem. Form the active species list at temperature $T$ with neutrino input $\nu$, map each entry to its energy-density weight (DOF, or $(7/8)\cdot\mathrm{DOF}$ for fermions), and sum the resulting rational list. No tactics; the arithmetic is discharged later by native_decide at concrete $T$ values.
why it matters
This is the shared kernel behind the default minimal-neutrino $g_{\star}(T)$ (specialized by fixing $\nu$ to the minimal species) and the Dirac high-T evaluation $g_{\star}(\nu_{\mathrm{Dirac}},200)=112$. The branch-gap theorem then shows the two conventions differ only through the neutrino term: the high-T gap is $(7/8)\cdot 6=21/4=5.25$.
It closes the review point that the repository lacked $g_{\star}(T)$ and threshold decoupling, while staying honest that particle content and mass thresholds are imported SM bookkeeping (gauge group and generation count RS-sourced elsewhere). Downstream spot checks recover the textbook high-T value $427/4=106.75$ and match the Dirac assembly in RelativisticDOF. The definition does not itself touch the forcing chain (T0–T8) or the mass ladder; it supplies the cosmological DOF input those layers feed when epochs matter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.