quark_dof_eq
plain-language theorem explainer
Quark helicity states total exactly 72: six flavours, three colours, two spins, and particle plus antiparticle. Cosmologists deriving the high-T effective degrees of freedom g_⋆ cite this as the quark piece of g_f. The proof unfolds the product definition and closes by native arithmetic decision.
Claim. The quark degree-of-freedom count equals $72$, i.e. $n_{\mathrm{flavours}}\times n_{\mathrm{colours}}\times n_{\mathrm{spin}}\times n_{\mathrm{p/\bar p}}=6\times 3\times 2\times 2=72$.
background
In the high-temperature regime above the electroweak transition, every Standard Model species is relativistic and unsuppressed, so $g_\star=g_b+(7/8)g_f$ is fixed by a pure helicity count. This module replaces the hand-entered constant $g_\star=106.75$ by an explicit bosonic and fermionic tally forced by the $Q_3$ chord-cube SM content.
Quark DOF are defined as the product of four natural-number factors: six flavours (u,d,c,s,t,b), three colours, two spin/helicity states (both helicities for massive Dirac fermions, and for above-EW relativistic counting), and a particle/antiparticle factor of two. The definition is therefore purely multiplicative over those constants; no phase-space integrals enter at this stage.
proof idea
One-step arithmetic certificate. Unfold quark_dof together with the four factor definitions (n_quark_flavours, n_colours, n_spin_states, n_particle_antiparticle), obtaining the concrete product $6\cdot 3\cdot 2\cdot 2$. Close with decide, which evaluates the natural-number equality to $72$.
why it matters
Feeds directly into fermionic_dof_eq, whose doc-comment states the fermion total $72+12+6=90$. That fermionic total, with the bosonic $g_b=28$ and the exact Boltzmann weight $7/8$, yields the rational $g_\star=427/4=106.75$ that matches the existing baryogenesis constant. The count is the quark half of the module's claim that SM particle content (and hence $g_\star$) is forced rather than inserted by hand. No deeper RS landmark (T5–T8, RCL, phi-ladder) is invoked here; the result is pure combinatorial bookkeeping inside the cosmology bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.