fermion_dof_per_gen_dirac_eq
plain-language theorem explainer
In the thermalized Dirac-neutrino branch, each fermion generation contributes exactly 32 relativistic degrees of freedom. Anyone assembling g_f or g_star under Dirac neutrinos cites this equality. The proof is a one-line native_decide on the sum of quark, charged-lepton, and Dirac-neutrino per-generation counts.
Claim. The per-generation fermion degree-of-freedom count in the thermalized Dirac-neutrino branch equals $32$: $$g_{f/\mathrm{gen}}^{(\mathrm{Dirac})} = g_{q/\mathrm{gen}} + g_{\ell^\pm/\mathrm{gen}} + g_{\nu/\mathrm{gen}}^{(\mathrm{Dirac})} = 32.$$
background
This module performs textbook high-temperature Standard Model bookkeeping for $g_\star = g_b + (7/8)g_f$, with RS-sourced inputs only for the gauge group, the generation count $3$, and the Fermi/Bose sign. Matter representations and the neutrino convention are imported physics, not RS predictions.
The Dirac branch treats neutrinos as fully thermalized Dirac fermions (4 DOF each: particle/antiparticle $\times$ two helicities), unlike the minimal left-handed Weyl convention (2 DOF). The definition being evaluated is the sum of three natural-number pieces: quark DOF per generation, charged-lepton DOF per generation, and Dirac-neutrino DOF per generation.
Upstream RS landmarks feeding the surrounding assembly (not this arithmetic line) include the gauge group from $Q_3$ cube automorphisms and three generations from face pairs in $D=3$. The $7/8$ thermal weight remains standard statistical mechanics.
proof idea
One-line computational proof: native_decide evaluates the closed natural-number definition
quark_dof_per_gen + charged_lepton_dof_per_gen + neutrino_dof_per_gen_dirac
and checks equality with $32$. No lemmas are invoked; the kernel reduces the arithmetic directly. Graph edges pointing at unrelated Gravity the identifiers are noise and play no role.
why it matters
Part of the Dirac-neutrino bookkeeping branch flagged in the module header: with three generations one obtains $g_f = 96$ and $g_\star = 112$ instead of the usual $90$ and $106.75$. The equality pins the per-generation building block so later totals stay exact rationals in Lean.
It does not advance the forcing chain (T0–T8), RCL, or mass-ladder results; status is honest SM bookkeeping over adopted representations. No downstream consumers are recorded in the graph yet; the immediate use is assembling total fermion DOF and the Dirac $g_\star$ figure. Open scope remains temperature dependence and threshold decoupling, handled elsewhere as $g_\star(T)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.