g_star_dirac_eq
plain-language theorem explainer
With fully thermalized right-handed Dirac neutrinos, the high-T relativistic effective degree count is exactly 112. Cosmologists comparing the minimal-neutrino SM value 106.75 to the Dirac branch cite this equality. The proof unfolds the weighted sum, substitutes the proved bosonic count 28 and Dirac fermionic count, then closes by rational arithmetic.
Claim. In the high-temperature Standard Model with thermalized right-handed Dirac neutrinos, the relativistic effective degree of freedom count equals $112$: $g_{*,\mathrm{Dirac}} = g_b + \frac{7}{8} g_{f,\mathrm{Dirac}} = 112$.
background
This module performs textbook high-$T$ SM bookkeeping for $g_* = g_b + (7/8) g_f$, valid only for $T \gtrsim T_{\mathrm{EW}}$ when all listed species are relativistic and thermally populated. The STATUS TAG is explicit: bookkeeping over adopted SM content, not a novel RS prediction.
RS supplies the gauge group $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ (from cube automorphisms), three generations (from $D=3$), and the Fermi–Dirac vs Bose–Einstein sign via spin-statistics. Imported physics includes the matter representations, the $7/8$ integral ratio from statistical mechanics, and the neutrino convention.
The default branch uses left-handed neutrinos only ($g_f = 90$), giving $g_* = 106.75$. The Dirac branch thermalizes right-handed partners as well, raising the fermionic helicity count and producing $g_* = 112$. Upstream, bosonic_dof_eq fixes the bosonic side at the standard $28$ (gauge polarizations plus Higgs).
proof idea
Short tactic proof. Unfold the Dirac $g_*$ definition and the Fermi–Dirac thermal weight $7/8$. Rewrite with the upstream equality that bosonic degrees of freedom equal $28$, and with the sibling equality for the Dirac fermionic helicity count. Finish with norm_num on the rational identity $28 + (7/8)\cdot g_{f,\mathrm{Dirac}} = 112$.
why it matters
Pins the Dirac-neutrino numerical endpoint so the module can treat the neutrino convention as a real model input rather than notation. Downstream, g_star_branch_gap uses this equality (with the minimal-branch value $106.75$) to prove the two branches differ by exactly $(7/8)\cdot 6 = 5.25$.
In the broader RS stack this sits under Standard Model assembly fed by GaugeFromCube and ParticleGenerations (three generations from $D=3$, eight-tick spin-statistics for the FD/BE sign). Cosmology modules that expose $g_*(T)$ and match the fixed high-$T$ constant against the derived bookkeeping rely on having both branches as proved rationals. It does not claim RS forces Dirac neutrinos; it only closes the arithmetic once that convention is chosen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.