gluons
plain-language theorem explainer
Records the deconfined gluon multiplet as a thermal species: massless, bosonic, with 16 internal degrees of freedom (8 adjoint colors times 2 helicities). Cosmology and SM bookkeeping cite it when assembling g_*(T) above the QCD crossover and when certifying the high-T bosonic count. The body is a four-field structure literal; no proof obligations.
Claim. The gluon thermal species is the record with name "gluons", mass threshold $0\,\mathrm{GeV}$, internal degree count $16$, and bosonic statistics ($\mathrm{fermion}=\mathrm{false}$). The count is the standard $8\times 2$ for the $SU(3)$ adjoint in the deconfined phase $T>T_{\mathrm{QCD}}$.
background
The module builds the textbook step-function $g_*(T)$: each species contributes its full relativistic DOF 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 content to hadrons. All arithmetic is exact over $\mathbb{Q}$.
A Species is a four-tuple: display name, mass threshold in GeV (rational PDG-rounded approximation; only order relative to $T$ matters), internal DOF count, and a fermion flag. Photons, neutrinos, quarks, and electroweak bosons are sibling literals in the same table.
Gluons enter only in the deconfined window. Below $T_{\mathrm{QCD}}$ they are replaced by pions in the hadronic list; the module does not model lattice crossover tails or Boltzmann suppression near threshold.
proof idea
Pure definition: the structure constructor packs the four fields "gluons", mass $0$, DOF $16$, and fermion := false. No lemmas, tactics, or obligations. The factor $8\times 2$ is documentary (adjoint dimension of $SU(3)$ times two massless polarizations) and is not re-derived here.
why it matters
Feeds the QGP species list (qgp_species := [gluons, up, down, strange]), which drives the strong-sector branch of $g_*(T)$ above $T_{\mathrm{QCD}}$. Downstream SM certificates (GStarCert, gStarCert) pin gluon_dof = 16 as part of the high-T bosonic total of 28, matching the bridge to RelativisticDOF.g_star_derived. Confinement modules (gluon_confinement, confinement_from_ledger) and the Yang–Mills mass-gap stub cite the same multiplet when arguing that colored adjoint modes do not appear as free asymptotic states. Within RS this is imported SM bookkeeping (gauge-group dimension is RS-aligned via three colors), not a $\phi$-ladder mass prediction; masses here are ordering thresholds only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.