quark_dof
plain-language theorem explainer
Counts relativistic quark helicity states as six flavours times three colours times two spins times particle plus antiparticle, equalling 72. Cosmologists deriving the high-T effective DOF g_⋆ cite this as the quark piece of g_f. It is a pure product of four named natural-number constants, with no proof obligation beyond the arithmetic identity proved downstream.
Claim. The quark contribution to the relativistic fermionic degrees of freedom is the natural number $N_q = 6 \times 3 \times 2 \times 2$, i.e. six quark flavours, three colours, two spin (helicity) states, and a particle/antiparticle factor of two.
background
The module derives the high-temperature Standard Model value $g_\star = 106.75$ by explicit helicity counting rather than inserting the number by hand. Above the electroweak transition every SM species is relativistic, so $g_\star = g_b + (7/8) g_f$ with $g_b = 28$ and $g_f = 90$, giving the exact rational $427/4$.
Quark counting uses four fixed factors: $n_{\mathrm{flavours}} = 6$ (u,d,c,s,t,b), $n_{\mathrm{colours}} = 3$, $n_{\mathrm{spin}} = 2$ (both helicities for Dirac fermions in the above-EW count), and $n_{\mathrm{p}\bar{\mathrm{p}}} = 2$. The product is the standard textbook quark DOF total of 72, which then enters the total fermionic sum alongside charged leptons and neutrinos.
proof idea
Definitional abbreviation only: the body is the four-factor product of the sibling constants for quark flavours, colours, spin states, and particle/antiparticle. No tactics or lemmas are invoked at this site. The numerical identity $N_q = 72$ is discharged later by quark_dof_eq via unfold and decide.
why it matters
Supplies the quark term inside fermionic_dof (total $g_f$ over all three generations) and is unfolded in the closing theorem g_star_derived_eq, which proves $g_\star^{\mathrm{derived}} = 427/4$. The companion lemma quark_dof_eq records the concrete evaluation $6\times 3\times 2\times 2 = 72$. Together these replace the hand-entered constant in BaryonAsymmetryDerivation with an explicit SM helicity count forced by the Q₃ chord-cube particle content. The result is pure bookkeeping inside the cosmology bridge; it does not itself invoke the T0–T8 forcing chain, but it makes the baryogenesis $g_\star$ input fully derived rather than postulated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.