hadron_species
plain-language theorem explainer
Defines the strong-sector content of the confined phase as the singleton list of pions. Cosmologists computing the step-function g_*(T) cite it whenever T sits below the QCD threshold. The body is a one-line list literal over the Species record.
Claim. The hadronic-phase strong-sector species list is the singleton $[\pi]$, where $\pi$ is the pion multiplet (mass $\approx 0.135$–$0.140\,\mathrm{GeV}$, $3$ bosonic degrees of freedom).
background
The module builds the standard instantaneous-threshold step function $g_*(T)$ over adopted SM content. Each thermal species is a record with name, rational mass threshold in GeV (only order relative to $T$ matters), internal DOF count, and a fermion flag. Above $T_{\mathrm{QCD}}\approx 0.15,\mathrm{GeV}$ the strong sector is quark–gluon plasma; below it, confined hadrons.
The pion entry used here is the confined-phase multiplet $\pi^+,\pi^-,\pi^0$ with mass $27/200$ GeV, three bosonic DOF. Masses are PDG-rounded rationals imported as ordering thresholds only; RS $\varphi$-ladder mass modules predict them independently elsewhere. Particle bookkeeping matches StandardModel.RelativisticDOF (gauge group and generation count RS-derived; representations and the $7/8$ fermionic weight imported).
proof idea
Pure definition: a list literal whose single element is the already-defined pion species record. No proof obligations, no lemmas applied.
why it matters
Closes the low-$T$ branch of the strong-sector switch inside the active-species selector. That selector builds [photon, neutrinos] ++ EW species with $m<T$ ++ (QGP if $T_{\mathrm{QCD}}<T$, else hadrons with $m<T$), which is the content table for the step-function $g_(T)$. Without this list the confined-phase evaluation would be empty and textbook spot checks below $T_{\mathrm{QCD}}$ would fail. It answers the external-review gap that the repository lacked temperature-dependent $g_$ and epoch-dependent particle content, while staying inside the honest MODEL (step) scope rather than lattice QCD EOS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.