fermion_dof_per_gen
plain-language theorem explainer
Defines the total relativistic fermion degrees of freedom in one Standard Model generation as the sum of quark, charged-lepton, and neutrino contributions (24 + 4 + 2). Cosmology and SM bookkeeping cite it when assembling g_f and g_star. The body is a three-term natural-number sum of the sibling per-sector counts.
Claim. The fermion degree-of-freedom count per generation is $g_{f,\mathrm{gen}} := g_{q,\mathrm{gen}} + g_{\ell^\pm,\mathrm{gen}} + g_{\nu,\mathrm{gen}}$, where the quark, charged-lepton, and (left-handed) neutrino per-generation counts are the standard SM tallies $24$, $4$, and $2$.
background
This module performs exact rational bookkeeping for the high-temperature Standard Model effective relativistic degrees of freedom $g_\star = g_b + (7/8) g_f = 106.75$. The status tag is explicit: textbook SM content assembled in Lean, not a novel Recognition Science prediction. The count applies only for $T \gtrsim T_{\mathrm{EW}}$, where every listed species is relativistic and thermally populated.
Per generation the matter sector splits into three blocks already defined upstream: quarks at $2$ flavors $\times$ $3$ colors $\times$ $2$ chiralities $\times$ $2$ (particle/antiparticle) $= 24$; charged leptons at $1 \times 2 \times 2 = 4$; neutrinos in the minimal SM convention (left-handed only) at $1 \times 1 \times 2 = 2$. RS supplies the gauge group and the generation count $3$ from $D=3$ face-pairs; the representation content and the left-handed neutrino convention are imported SM data.
proof idea
Definitional abbreviation: the value is the sum of the three sibling natural-number definitions quark_dof_per_gen, charged_lepton_dof_per_gen, and neutrino_dof_per_gen. No tactics or lemmas; evaluation is ordinary Nat arithmetic once those three constants are unfolded.
why it matters
This is the per-generation brick in the fermionic half of $g_\star$. Downstream, fermion_dof_per_gen_eq certifies the concrete value $30$ by native_decide, and fermionic_dof multiplies by the RS-sourced generation count to obtain total $g_f = 3 \times 30 = 90$, which enters $g_\star = 28 + (7/8)\cdot 90 = 106.75$.
In the Recognition framework the generation factor $3$ is not free: it is forced as face-pairs of the cube from $D=3$ (forcing chain T8 and ParticleGenerations). The gauge factors behind the quark color count come from Q₃ automorphisms (GaugeFromCube). The Fermi–Dirac thermal weight $7/8$ is standard statistical mechanics; RS only fixes the bosonic/fermionic sign via spin-statistics. The module is honest bookkeeping over adopted SM representations, not a derivation of those representations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.