fermionic_dof_eq
plain-language theorem explainer
The Standard Model fermionic helicity count is exactly 90: 72 quarks + 12 charged leptons + 6 neutrinos, summed over three generations. Cosmologists deriving g_⋆ and η_B from Q₃-forced particle content cite this equality. The proof unfolds the sum definition and rewrites with the three sector equalities already decided by arithmetic.
Claim. The total fermionic relativistic degree-of-freedom count equals $90$, namely $g_f = g_{\mathrm{quarks}} + g_{\mathrm{charged\,leptons}} + g_{\nu} = 72 + 12 + 6$.
background
In the high-temperature regime above the electroweak transition, every Standard Model species is relativistic and unsuppressed. The effective relativistic DOF is $g_\star = g_b + (7/8) g_f$. This module derives that number from explicit SM counting forced by Q₃ chord-cube content, rather than leaving $g_\star = 106.75$ as a hand-entered constant.
Fermionic DOF is defined as the sum of three sector counts: quarks ($6$ flavours $\times$ $3$ colours $\times$ $2$ spin $\times$ $2$ particle/antiparticle $= 72$), charged leptons ($3 \times 2 \times 2 = 12$), and neutrinos ($3$ flavours $\times$ $1$ helicity $\times$ $2$ particle/antiparticle $= 6$). The three sector equalities quark_dof_eq, charged_lepton_dof_eq, and neutrino_dof_eq are already proved by unfolding the multiplicity definitions and decide.
The module works in exact rational arithmetic; the fermionic total is the integer half of the $g_\star$ formula before the $7/8$ Boltzmann weight is applied.
proof idea
Unfold the definition of total fermionic DOF as the sum of quark, charged-lepton, and neutrino contributions. Rewrite each summand by the corresponding sector theorem (quark_dof_eq gives $72$, charged_lepton_dof_eq gives $12$, neutrino_dof_eq gives $6$). The resulting numeral identity $72+12+6=90$ closes by definitional reduction; no further tactics are needed.
why it matters
This is the fermionic half of the $g_\star = 106.75$ derivation: with $g_b = 28$ and the exact Fermi–Dirac factor $7/8$, one obtains $28 + (7/8)\cdot 90 = 427/4$. It is packaged into gStarDerivationCert and mirrored in StandardModel.RelativisticDOF (gStarCert, g_star_derived_eq, fermionic_traces_to_Q3).
Downstream, EtaBExactRungDerivation uses $g_f = 90$ to obtain the baryon-asymmetry rung $-44$ and the identity that half the fermionic count equals the dimension gap $45$ at $D=3$ (T8). That bridge ties SM fermion content to the forcing-chain spatial dimension, so matter and antimatter each carry one full gap worth of fermions.
The count is the Q₃-forced SM content the module advertises: three generations, three colours, and the usual spin and particle/antiparticle multiplicities, with left-handed neutrinos only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.