strange
plain-language theorem explainer
Defines the strange quark as a thermal species for the step-function g_*(T): name "strange", mass threshold 0 GeV, 12 internal degrees of freedom, fermionic. Cosmology and mass-hierarchy modules cite it when assembling quark–gluon plasma content above T_QCD. The body is a four-field structure literal.
Claim. The strange quark (deconfined phase) is the thermal species with name $\mathrm{strange}$, mass threshold $0\,\mathrm{GeV}$, $g=12$ internal degrees of freedom, and fermionic statistics. The mass field is the ordering threshold used by $g_*(T)$; the physical $m_s\approx 95\,\mathrm{MeV}$ lies below $T_{\mathrm{QCD}}$, so the species is fully active whenever the QGP list is selected.
background
The module builds the standard instantaneous-threshold $g_*(T)$ over adopted SM content: 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). Arithmetic is exact over $\mathbb{Q}$.
A Species record packages four fields: a display name, a rational mass threshold in GeV (only order relative to $T$ matters), an internal DOF count, and a fermion/boson flag (fermions enter with the usual $7/8$ factor). Masses are PDG-rounded imports used only as ordering cuts; RS $\varphi$-ladder modules predict them independently elsewhere.
Strange is one of the light quarks kept in the deconfined list. With $m_s\approx 95,\mathrm{MeV}<T_{\mathrm{QCD}}$, it remains relativistic throughout the QGP window, so its threshold is recorded as $0$ and activation is controlled by list membership rather than a per-species mass cut.
proof idea
Pure definition: the four-tuple constructor of Species is applied with name $\mathrm{strange}$, mass $0$, dof $12$, and fermion flag true. No lemmas or tactics.
why it matters
Feeds the QGP species list (qgp_species = [gluons, up, down, strange]), which is the strong-sector content of $g_(T)$ above $T_{\mathrm{QCD}}$. That list is the module's answer to the external review point that the repository lacked a temperature-dependent $g_$ with threshold decoupling and epoch-dependent particle content.
Downstream mass infrastructure also names the strange quark: the SM fermion inductive, charge/rung/sector maps, positivity of the predicted strange mass, and the down-quark mass hierarchy tables. Those uses sit in the $\varphi$-ladder mass formula (yardstick $\times\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) rather than in cosmology, but they share the same SM species label.
Within the forcing chain this is bookkeeping, not a T0–T8 step: gauge group and generation count are RS-derived upstream; matter representations and the $7/8$ factor remain imported SM content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.