down
plain-language theorem explainer
Registers the deconfined down quark as a thermal species with vanishing mass threshold, 12 internal degrees of freedom, and fermionic statistics for the step-function g_*(T). Cosmology code that assembles the quark–gluon-plasma species list cites it. The body is a pure structure literal; there is nothing to prove.
Claim. The deconfined down quark is the thermal species with name $\mathrm{down}$, mass threshold $0\,\mathrm{GeV}$, $12$ internal degrees of freedom, and fermionic statistics.
background
The module builds the standard instantaneous-threshold model of $g_*(T)$: each species contributes its full relativistic DOF count while $T$ exceeds its mass threshold and drops out below it. At $T_{\mathrm{QCD}}\approx 0.15,\mathrm{GeV}$ the strong sector switches from quark–gluon plasma (gluons + $u,d,s$) to hadrons (pions). All arithmetic is exact over $\mathbb{Q}$.
A Species record packages a name, a rational mass threshold in GeV (only order relative to $T$ matters), an internal DOF count, and a fermion/boson flag. The down entry is the deconfined light quark: mass threshold $0$ so it is always on above $T_{\mathrm{QCD}}$, and $12$ DOF from $3$ colors $\times$ $2$ spins $\times$ particle/antiparticle. Particle content and the $7/8$ fermionic weight are the same imported SM bookkeeping as RelativisticDOF.
proof idea
No proof. The definition is the four-field structure literal $\langle\mathrm{``down''},,0,,12,,\mathrm{true}\rangle$ inhabiting Species.
why it matters
Supplies the down-quark row in the QGP table. Downstream, qgp_species is exactly [gluons, up, down, strange], so every high-$T$ strong-sector $g_*$ evaluation and the bridge to RelativisticDOF.g_star_derived depends on this constant.
The module exists to close the external-review gap that RS fixed a single $g_*$ without a temperature-dependent threshold function. This entry is pure SM bookkeeping (PDG-rounded thresholds, standard DOF counts), not a $\varphi$-ladder mass derivation; masses come from IndisputableMonolith.Masses elsewhere and are used here only as ordering cuts. It does not touch T5–T8 or the RCL; it is cosmology infrastructure under the adopted SM content tag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.