fermionic_dof_dirac_eq
plain-language theorem explainer
In the thermalized Dirac-neutrino branch of the SM relativistic degree count, total fermionic DOF equals 96. Anyone assembling g★ under right-handed neutrinos (versus the minimal left-handed convention) cites this equality. The proof is a one-line native decision that evaluates the product of three generations with the per-generation Dirac fermion count.
Claim. The total number of fermionic relativistic degrees of freedom in the thermalized Dirac-neutrino convention equals $96$.
background
The module StandardModel.RelativisticDOF performs textbook high-temperature SM bookkeeping for $g_\star = g_b + (7/8)g_f$, valid only for $T \gtrsim T_{\mathrm{EW}}$. RS supplies the gauge group SU(3)×SU(2)×U(1) (from Q₃ automorphisms) and the generation count 3 (from $D=3$); matter representations and the 7/8 thermal weight are imported standard physics, not RS predictions.
Two neutrino conventions are tracked. The minimal (left-handed only) branch has $g_f = 90$ and $g_\star = 106.75$. The Dirac branch thermalizes right-handed neutrinos as well, adding six fermionic DOF and raising $g_f$ to 96. The definition of the Dirac fermionic total is the product of the generation count with the per-generation Dirac fermion DOF; this theorem pins that product at 96.
proof idea
One-line computational proof via native_decide. The tactic reduces the Dirac fermionic total (defined as generations times per-generation Dirac DOF) and evaluates the resulting natural-number expression to 96. No intermediate lemmas are invoked beyond definitional unfolding and kernel arithmetic.
why it matters
Feeds directly into g_star_dirac_eq, which proves $g_\star = 112$ when right-handed Dirac neutrinos are thermalized. That parent unfolds the Dirac $g_\star$ formula, rewrites with the bosonic DOF identity and this fermion identity, then finishes by norm_num. The module records that the two branches differ by $(7/8)\cdot 6 = 5.25$.
Within Recognition Science this remains status-tagged BOOKKEEPING over adopted SM content: the gauge group and three generations are RS-sourced (T8 / ParticleGenerations), but the representation content and the Dirac-versus-minimal choice are imported. It closes the Dirac side of the high-T assembly so cosmology modules can cite an exact rational alternative to 106.75.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.