activeWith
plain-language theorem explainer
Lists every Standard Model thermal species that remains relativistic at temperature T (GeV), with the neutrino sector passed in explicitly so minimal and Dirac conventions share one filter. Cosmologists computing g_★(T) cite it as the active-content step before summing weighted degrees of freedom. The body is a pure list concatenation: photon plus the chosen neutrinos, electroweak species below their mass thresholds, and either QGP or hadronic content according to T versus T_QCD.
Claim. Given a neutrino-sector species $\nu$ and a temperature $T\in\mathbb{Q}$ (GeV), return the list of thermal species that are relativistic and populated at $T$: the photon, $\nu$, every electroweak-sector species with mass strictly less than $T$, and either the quark–gluon-plasma species (if $T_{\mathrm{QCD}}<T$) or the hadronic species with mass less than $T$ (otherwise).
background
The module implements the textbook instantaneous-threshold model of $g_\star(T)$: each species contributes its full relativistic degree count while $T$ exceeds its mass and drops out below it, with the QCD transition at $T_{\mathrm{QCD}}\approx 0.15,\mathrm{GeV}$ switching the strong sector from QGP (gluons + $u,d,s$) to hadrons (pions). Valid domain is $T\gtrsim 1,\mathrm{MeV}$.
A Species carries a name, mass threshold in GeV (rational PDG approximation; only order relative to $T$ matters), internal DOF count, and fermion/boson flag. Fixed tables supply the photon, electroweak ladder (top through electron), QGP content, and hadronic content. Neutrinos are not hard-wired: the caller supplies either the minimal-SM or Dirac species so both conventions reuse one filter.
Upstream high-$T$ bookkeeping fixes $g_\star=106.75$ above the electroweak scale (bosons 28, fermions 90 with the $7/8$ weight). This definition is the temperature-dependent content layer that feeds the weighted sum.
proof idea
Pure definition, no proof obligations. Concatenate three pieces: the always-active pair [photon, nu]; the electroweak list filtered by mass < T; and a branch on T_QCD < T that inserts the full QGP list or else the hadronic list filtered by mass < T. No lemmas are applied; the construction is the step-function content model itself.
why it matters
Direct input to g_starWith, which maps each active species to its energy-density weight and sums to the rational g_★(T). The default g_star is the specialization g_starWith neutrinos. The module exists to answer the external review that RS fixed a single g_★ number without a temperature-dependent function, threshold decoupling, or epoch-dependent particle content. Spot-check theorems later in the file recover the textbook values (e.g. 427/4 at T = 200 GeV). Masses are imported thresholds only; RS φ-ladder mass modules predict them independently and are not re-derived here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.