fermionic_dof
plain-language theorem explainer
Total SM fermionic relativistic degrees of freedom equal three generations times thirty DOF per generation, hence ninety. Cosmology and unification modules cite this integer in the high-T g_star assembly and in the fermionic route to the η_B rung −44. The body is a one-line product of the generation count by the per-generation fermion tally.
Claim. Define the total fermionic relativistic degree count by $g_f := N_{\mathrm{gen}} \cdot g_{f/\mathrm{gen}}$, where $N_{\mathrm{gen}}$ is the generation count (three, from $Q_3$ face-pairs at $D=3$) and $g_{f/\mathrm{gen}}$ is the per-generation fermion DOF (quarks plus charged leptons plus neutrinos). Numerically $g_f = 3 \times 30 = 90$ in the minimal-neutrino convention.
background
The module assembles the textbook high-temperature Standard Model count $g_\star = g_b + (7/8) g_f = 28 + (7/8)\cdot 90 = 106.75$ as exact rational arithmetic. Status is honest bookkeeping over adopted SM content, valid only for $T \gtrsim T_{\mathrm{EW}}$ where all listed species are relativistic.
RS supplies the gauge group from cube automorphisms and the generation count $N_{\mathrm{gen}} = \mathrm{face_pairs}(3) = 3$ from $D=3$. The per-generation fermion tally sums quark, charged-lepton, and neutrino DOF under the minimal-neutrino convention (left-handed only, two DOF per generation). Matter representations and the $7/8$ Fermi–Dirac weight are imported standard physics, not RS-derived.
Sibling definitions fix bosonic pieces (gluons, weak bosons, Higgs) so that $g_b=28$. Parallel defs in Cosmology.GStarDerivation and Unification.FermionDOFGapBridge restate the same total $g_f=90$ by species sum or by $3\times 30$.
proof idea
Pure definition: the natural-number product of the local generation count by the local per-generation fermion DOF. No tactics, no lemmas. Unfolding both factors and the species sums underneath yields the integer ninety, which downstream equality theorems discharge by native_decide or decide.
why it matters
This integer is the fermionic half of the $g_\star=106.75$ bookkeeping identity and the input to several cosmology bridges. Downstream, eta_B_rung_from_fermionic sets the rung to $A - g_f/2 = 1-45=-44$, and fermionic_half_equals_gap identifies $g_f/2$ with the dimension gap at $D=3$. The EtaBExactRungCert structure records that this fermionic route agrees with the gap-from-dimension and chirality-torsion routes on the integer $-44$ (shared arithmetic content, not independent empirical confirmations; the assignment of that rung to $\eta_B$ remains hypothesis-grade).
In the Recognition chain the generation factor is the RS-sourced piece (T8 forces $D=3$, face-pairs give three generations). The factor thirty per generation is SM representation bookkeeping. The module explicitly flags the Dirac-neutrino branch ($g_f=96$, $g_\star=112$) as an alternate convention, not used here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.