quark_dof_per_gen_eq
plain-language theorem explainer
Per Standard Model generation the quark sector contributes exactly 24 relativistic degrees of freedom: two flavors, three colors, two chiralities, and particle plus antiparticle. Anyone assembling the high-T g_star bookkeeping cites this equality. The proof is a one-line native evaluation of the defining product.
Claim. The quark degrees of freedom per generation equal $24$, where that quantity is the product (flavors per generation) $\times$ (colors) $\times$ (chiralities) $\times$ (particle/antiparticle factor).
background
This module performs exact rational bookkeeping for the high-temperature Standard Model effective relativistic count $g_\star = g_b + (7/8)g_f = 106.75$, valid only for $T \gtrsim T_{\mathrm{EW}}$. Status is honest bookkeeping over adopted SM content, not a novel RS prediction.
Quark DOF per generation is defined as the product of four natural-number factors: flavors per generation (up- and down-type), colors ($N_c = 3$), chiralities (left and right, fixed at 2), and the particle/antiparticle factor (also 2). The chirality constant is the local def equal to 2. RS supplies the gauge group and the generation count 3 upstream; the matter representation content (which reps the quarks sit in) is imported SM input.
proof idea
One-line tactic proof: native_decide evaluates the closed natural-number product that defines quark DOF per generation and checks equality with 24. No lemmas beyond the defining unfold of that product and the constant chiralities = 2 are required; the arithmetic is decided by the kernel.
why it matters
The equality pins the quark contribution that feeds the fermionic half of $g_\star$. With three generations the quarks alone supply $3 \times 24 = 72$ of the $g_f = 90$ fermionic DOF in the minimal-neutrino convention, so the rational identity $g_\star = 427/4$ rests on this factor being exactly 24.
In the RS ledger this sits under Standard Model bookkeeping: gauge group from cube automorphisms and three generations from $D = 3$ are RS-sourced, while the representation multiplicities (flavors, colors, chiralities) remain imported. No downstream theorems currently depend on it in the curated graph; it is a local certification step inside the $g_\star$ assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.