fermionic_dof_dirac
plain-language theorem explainer
Total fermionic relativistic degrees of freedom in the thermalized-Dirac-neutrino branch equal generations times DOF per generation, fixed at 96. Cosmologists and SM bookkeepers cite it when assembling g_star with right-handed neutrinos thermally active. The body is a one-line product of the generation count and the per-generation Dirac fermion tally.
Claim. Define the total fermionic relativistic degree-of-freedom count in the thermalized-Dirac-neutrino branch by $g_f^{\mathrm{Dirac}} := N_{\mathrm{gen}} \times g_{f/\mathrm{gen}}^{\mathrm{Dirac}}$, where $N_{\mathrm{gen}} = 3$ and $g_{f/\mathrm{gen}}^{\mathrm{Dirac}} = 32$, so $g_f^{\mathrm{Dirac}} = 96$.
background
The module performs exact rational bookkeeping for the high-temperature Standard Model effective relativistic degree count $g_\star = g_b + (7/8) g_f$. Scope is textbook SM content above the electroweak scale: all listed species relativistic and thermally populated. It is not a novel RS prediction.
RS-derived inputs used here are the generation count $N_{\mathrm{gen}} = 3$ (from $Q_3$ face-pairs at $D = 3$) and the gauge group from cube automorphisms. The Dirac branch differs from the minimal-neutrino convention by counting thermalized right-handed neutrinos, giving 32 fermion DOF per generation (quarks + charged leptons + Dirac neutrinos) rather than the usual 30.
Upstream, fermion_dof_per_gen_dirac assembles that per-generation 32, and several n_generations aliases fix the factor 3.
proof idea
Pure definition: the natural-number product of the generation count and the per-generation Dirac fermion DOF. No tactics or lemmas; evaluation is deferred to the sibling equality theorem that discharges the product to 96 by native_decide.
why it matters
Supplies the $g_f$ factor for the Dirac-neutrino branch of $g_\star$. Downstream, the equality theorem records $g_f^{\mathrm{Dirac}} = 96$, and g_star_dirac builds $g_\star = g_b + (7/8),g_f^{\mathrm{Dirac}}$, documented as 112 when right-handed Dirac neutrinos are thermalized.
In the module's assembly, this is the Part-5 alternative to the default $g_f = 90$ (minimal left-handed neutrinos only). Framework landmarks touched are the RS-sourced generation count from $D = 3$ face-pairs and the spin-statistics sign that selects Fermi-Dirac weighting; the representation content and the $7/8$ integral remain imported SM/stat-mech inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.