ew_species
plain-language theorem explainer
Named list of Standard Model electroweak-sector thermal species used as mass-threshold inputs to the step-function g_*(T). Cosmologists computing temperature-dependent relativistic degrees of freedom cite it when filtering which EW particles remain relativistic. The body is a fixed list literal of nine predeclared Species records (top through electron).
Claim. The electroweak-sector species table is the ordered list of thermal species $\{t, H, Z, W, b, \tau, c, \mu, e\}$, each carrying a PDG-rounded mass threshold in GeV, an internal degree-of-freedom count, and a fermion/boson flag. These species decouple stepwise as the plasma temperature $T$ falls below their masses.
background
The module implements the textbook instantaneous-threshold model of $g_*(T)$: each species contributes its full relativistic DOF count while $T$ exceeds its mass and drops out below it. A Species record holds a name, rational mass (GeV), natural DOF count, and a fermion flag (for the $7/8$ factor).
Masses are imported PDG-rounded rationals used only as ordering thresholds; the $\varphi$-ladder mass modules predict them independently elsewhere. Below $T_{\mathrm{EW}}$ the bosonic sector is counted in the broken phase (massive $W/Z$ with 3 polarizations, one physical Higgs).
Sibling entries supply the concrete records: top, Higgs ($m\approx 125,\mathrm{GeV}$, 1 DOF), $Z$, $W$, bottom ($m\approx 4.2,\mathrm{GeV}$, 12 DOF), tau, charm, muon, and electron ($m\approx 0.511,\mathrm{MeV}$, 4 DOF).
proof idea
Pure definition: a list literal assembling the nine already-declared electroweak Species constants in descending-mass order. No proof obligations, lemmas, or tactics.
why it matters
Feeds activeWith, which builds the relativistic species present at temperature $T$ by retaining photon and neutrinos, filtering this EW list by s.mass < T, and switching the strong sector at $T_{\mathrm{QCD}}$. That active list is the backbone of the module's $g_*(T)$ step function, written to answer the external review that RS lacked temperature-dependent particle content.
The construction stays inside the honest MODEL scope: leading step-function approximation over adopted SM content, valid for $T\gtrsim 1,\mathrm{MeV}$. It does not touch the forcing chain (T0–T8) or RCL; it is bookkeeping that lets high-$T$ $g_*$ match the derived SM value via the bridge theorem noted in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.