top
plain-language theorem explainer
Named constant for the top quark as a thermal species: mass threshold 173 GeV, 12 internal DOF, fermionic. Cosmology code that builds g_*(T) step functions cites it when assembling electroweak-sector content. The body is a four-field structure literal; no proof obligations.
Claim. The top quark is the thermal species with name $\mathrm{top}$, mass threshold $m = 173\,\mathrm{GeV}$, internal degrees of freedom $g = 12$ (3 colors $\times$ 2 spins $\times$ particle/antiparticle), and fermionic statistics.
background
The module implements the standard instantaneous-threshold model of $g_*(T)$: each species contributes its full relativistic DOF count while $T$ exceeds its mass and drops out below that threshold, with a QCD switch at $T_{\mathrm{QCD}} \approx 0.15,\mathrm{GeV}$. Masses are PDG-rounded rationals used only for ordering against $T$; the $\varphi$-ladder mass modules predict them independently elsewhere.
A Species record packages four fields: a display name, a rational mass threshold in GeV, a natural number of internal degrees of freedom, and a Boolean fermion flag (fermions enter $g_*$ with the usual $7/8$ factor). The top entry is one row in the imported SM bookkeeping table that feeds the electroweak list and the high-$T$ bridge to RelativisticDOF.g_star_derived.
proof idea
Pure definition: the four-tuple constructor of Species is applied to the string $\mathrm{top}$, the rational $173$, the natural $12$, and true (fermion). No lemmas, tactics, or obligations.
why it matters
Supplies the heaviest SM fermion threshold in the electroweak species list (ew_species: top, Higgs, $Z$, $W$, bottom, tau, charm, muon, electron). That list drives the step-function $g_(T)$ above and below the electroweak scale, so the top mass sets when the 12 fermionic DOF leave the relativistic count as the universe cools. Downstream rung-descent and $W$-mass ladder material reuse the same identifier only as a shared name token; the cosmological role is the threshold bookkeeping that answers the external review demand for a temperature-dependent $g_$ over adopted SM content. Does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is imported SM data ordered for decoupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.