fermionic_dof
plain-language theorem explainer
Defines the total Standard Model fermionic helicity count as the sum of quark, charged-lepton, and neutrino degrees of freedom across three generations. Cosmology and baryogenesis derivations cite it as the integer g_f entering g_⋆ = g_b + (7/8)g_f and the η_B rung route A − g_f/2. The body is a three-term natural-number sum of already-defined sector counts.
Claim. The total fermionic relativistic degrees of freedom are $g_f := g_q + g_{\ell^\pm} + g_\nu$, where $g_q$, $g_{\ell^\pm}$, and $g_\nu$ are the quark, charged-lepton, and neutrino helicity counts (all three generations, particle and antiparticle).
background
This module derives the high-temperature effective count $g_\star = 106.75$ from explicit Standard Model particle content forced by the $Q_3$ chord-cube structure, rather than leaving $g_\star$ as a hand-entered constant. Above the electroweak transition every SM species is relativistic, so $g_\star = g_b + (7/8) g_f$ with bosonic and fermionic helicity totals $g_b$ and $g_f$.
The fermionic side splits by sector. Quark DOF are flavours $\times$ colours $\times$ spins $\times$ (particle+antiparticle). Charged leptons drop colour. Neutrinos are left-handed only, so one helicity per flavour times particle/antiparticle. Sibling constants fix three generations, three colours, two spin states, and the particle/antiparticle factor of two.
Upstream, quark_dof, charged_lepton_dof, and neutrino_dof package those products; this definition only adds them. A parallel SM module states the same total as three generations times thirty DOF per generation.
proof idea
Definition, not a proof. The body is the natural-number sum of the three sector counts already defined in-module: quark DOF plus charged-lepton DOF plus neutrino DOF. No tactics, no lemmas. Downstream fermionic_dof_eq unfolds this sum and rewrites each summand to obtain $72+12+6=90$.
why it matters
Supplies the integer $g_f$ that closes the derived $g_\star$ certificate in this module: with $g_b=28$ and the Fermi–Dirac factor $7/8$, one gets the exact rational $427/4=106.75$, matching the baryogenesis constant. Downstream g_star_derived and GStarDerivationCert consume it directly.
It also feeds the η_B exact-rung stack. Route C sets the rung to $A - g_f/2$; with $g_f=90$ this is $1-45=-44$. The bridge fermionic_half_equals_gap identifies $g_f/2$ with the dimension gap at $D=3$, so matter and antimatter each carry one full gap worth of fermions. EtaBExactRungCert packages that agreement with the dimension and chirality routes (shared integer content, not independent empirical confirmations).
Landmark contact is T8 ($D=3$) via the gap identity, and the forced SM content that makes $g_f$ a derived rather than fitted integer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.