bottom
plain-language theorem explainer
Defines the bottom quark as a thermal species for the step-function g_*(T): mass threshold 21/5 GeV (≈ 4.2 GeV), 12 internal degrees of freedom, fermionic. Cosmology code that builds electroweak-sector species lists and temperature-dependent relativistic DOF counts cites it. The body is a four-field structure literal.
Claim. The bottom quark is the thermal species with name "bottom", mass threshold $m = 21/5$ GeV, $g = 12$ internal degrees of freedom, 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 it, with a QCD switch at $T_{\mathrm{QCD}} \approx 0.15$ GeV. Masses are PDG-rounded rationals used only for ordering against $T$; particle content follows SM bookkeeping from RelativisticDOF.
A Species is a four-tuple: display name, mass threshold in GeV (rational), internal DOF count, and a Boolean for fermion vs boson (fermions enter $g_*$ with the $7/8$ factor). The bottom entry uses $m = 21/5$ (≈ 4.2 GeV) and 12 DOF (3 colors × 2 spins × particle/antiparticle), marked fermionic.
proof idea
Pure definition: a structure value with fields "bottom", mass $21/5$, dof $12$, and fermion = true. No proof obligations.
why it matters
Feeds the electroweak species table ew_species (top, Higgs, Z, W, bottom, tau, charm, muon, electron), which drives the step-function $g_(T)$ below the electroweak scale. That table is the module's answer to the external review that RS lacked temperature-dependent $g_$ and threshold decoupling. Masses are imported thresholds only; RS $\varphi$-ladder mass modules predict them separately and are not re-derived here. Homonymous bottom identifiers elsewhere (trace falsehood, geometric edges) are unrelated name collisions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.