fermion_dof_per_gen_dirac
plain-language theorem explainer
Per-generation fermion relativistic degrees of freedom equal 32 when neutrinos are thermalized Dirac fields (both chiralities). The count is quarks 24 plus charged leptons 4 plus Dirac neutrinos 4. Cosmology and SM bookkeeping cite it when assembling g_f = 96 and the Dirac-branch g_star. The body is a three-term natural-number sum of the sector definitions.
Claim. Define the fermion relativistic degrees of freedom per generation in the thermalized Dirac-neutrino branch by $g_{f/\mathrm{gen}}^{\mathrm{Dirac}} := g_{q/\mathrm{gen}} + g_{\ell^\pm/\mathrm{gen}} + g_{\nu/\mathrm{gen}}^{\mathrm{Dirac}}$, i.e. the sum of the per-generation quark, charged-lepton, and Dirac-neutrino DOF counts (equaling $24+4+4=32$).
background
This module performs exact rational bookkeeping for the high-temperature Standard Model effective relativistic degree count $g_\star = g_b + (7/8)g_f$. Status is explicit: textbook SM content assembled in Lean, not a novel Recognition Science prediction. The single number $106.75$ applies only for $T \gtrsim T_{\mathrm{EW}}$; a Dirac-neutrino branch raises $g_f$ and yields $g_\star = 112$.
RS supplies the gauge group, the generation count $3$, and the Fermi vs Bose sign via spin-statistics. Matter representations, the $7/8$ integral ratio, and the high-$T$ scope are imported physics. This definition sits in the Dirac branch, where right-handed neutrinos are thermally populated.
Upstream sector counts: quarks give $2$ flavors $\times 3$ colors $\times 2$ chiralities $\times 2$ (particle/antiparticle) $= 24$; charged leptons give $1\times 2\times 2 = 4$; Dirac neutrinos likewise $1\times 2\times 2 = 4$.
proof idea
Definitional abbreviation, not a proved theorem. The body is the natural-number sum of three already-defined sector constants: per-generation quark DOF, charged-lepton DOF, and Dirac-neutrino DOF. No tactics or lemmas; evaluation to $32$ is discharged downstream by native_decide in the equality theorem.
why it matters
Closes the per-generation fermion tally on the thermalized-Dirac-neutrino branch so total $g_f$ can be formed as generations times this constant. Downstream, the equality theorem pins the value at $32$, and fermionic_dof_dirac multiplies by the generation count to obtain total fermion DOF $96$ (versus $90$ in the minimal left-handed-neutrino convention).
In the module assembly this feeds the Dirac-branch $g_\star$ path noted in the module doc ($g_f = 96$, $g_\star = 112$). Framework landmarks enter only indirectly: generation count $3$ from $D=3$ face pairs, and the Fermi weight sign from the eight-tick spin-statistics theorem; the representation arithmetic itself remains imported SM content. No open RS derivation is claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.