up
plain-language theorem explainer
Defines the deconfined up quark as a thermal species with mass threshold 0 GeV, 12 internal degrees of freedom, and fermionic statistics. Cosmology and g_*(T) bookkeeping cite it when assembling the quark–gluon plasma content above T_QCD. It is a four-field structure literal: name, rational mass, DOF count, fermion flag.
Claim. The deconfined up quark is the thermal species with name $\mathrm{up}$, mass threshold $m=0\,\mathrm{GeV}$ (current mass $\ll T_{\mathrm{QCD}}$), internal degrees of freedom $g=12$, and fermionic statistics.
background
The module builds the standard instantaneous-threshold step function $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 QGP (gluons + $u,d,s$) to hadrons (pions).
A Species is a thermal bookkeeping record: a name string, a rational mass threshold in GeV (only order relative to $T$ matters), a natural DOF count, and a Boolean fermion flag (for the $7/8$ fermionic weight). Masses are PDG-rounded imports used only as ordering thresholds; RS $\varphi$-ladder mass modules predict them independently elsewhere.
For a light Dirac quark the internal count is $2,(\mathrm{spin})\times 3,(\mathrm{color})\times 2,(\mathrm{particle/antiparticle})=12$. Setting the threshold to $0$ encodes that the current up mass lies far below $T_{\mathrm{QCD}}$, so the deconfined up stays relativistic throughout the QGP window.
proof idea
Pure definition: the four-tuple constructor of Species is filled with the string "up", mass $0$, DOF $12$, and fermion := true. No lemmas or tactics.
why it matters
Supplies the up-quark row in the QGP species table that feeds $g_*(T)$ above confinement. Downstream in-module consumer qgp_species aggregates gluons with $u,d,s$ for the high-$T$ strong sector; that content is what the module’s bridge theorems compare against RelativisticDOF.g_star_derived in the unbroken/broken electroweak counting.
The declaration is imported SM bookkeeping, not an RS derivation: gauge group and generation count are RS-derived upstream, while matter representations and the $7/8$ integral remain imported. It answers the external-review gap that the repo lacked a temperature-dependent $g_*(T)$ with threshold decoupling. It does not touch T5–T8, RCL, or the $\varphi$-ladder mass formula; those live in Foundation and Masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.