g_star_dirac
plain-language theorem explainer
Effective high-T relativistic DOF count when right-handed neutrinos are thermalized Dirac partners: bosonic DOF plus (7/8) times the Dirac-branch fermionic count. Cosmologists comparing the minimal-neutrino and Dirac branches of g_★ cite this assembly. The body is a one-line weighted sum; the numerical identity 112 is proved downstream.
Claim. Define $g_{\star}^{\mathrm{Dirac}} := g_b + \tfrac{7}{8}\, g_f^{\mathrm{Dirac}}$, where $g_b$ is the total bosonic relativistic degree count above the electroweak scale and $g_f^{\mathrm{Dirac}}$ is the fermionic count with three generations of thermalized right-handed Dirac neutrinos.
background
This module performs textbook high-temperature Standard Model bookkeeping for $g_\star$, valid only for $T \gtrsim T_{\mathrm{EW}}$ where every listed species is 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), the generation count $3$ (from $D=3$), and the Fermi–Dirac versus Bose–Einstein sign via the eight-tick spin-statistics theorem. Imported are the SM matter representations, the $7/8$ thermal weight (the standard integral ratio $\int x^3/(e^x+1),dx,/\int x^3/(e^x-1),dx$), and the neutrino convention.
The mainline count uses the minimal-neutrino convention ($g_f=90$, $g_\star=106.75$). This definition is the alternate branch: thermalized right-handed Dirac partners raise the fermionic count so that $g_f^{\mathrm{Dirac}}=96$ and $g_\star=112$. Bosonic DOF are assembled as gluons plus symmetric weak bosons plus Higgs; the Fermi–Dirac weight is the constant $7/8$.
proof idea
Pure definitional assembly, not a proof. Cast the natural-number bosonic count to $\mathbb{R}$, multiply the Dirac-branch fermionic count by the imported weight $7/8$, and add. No tactics, no lemmas. Downstream g_star_dirac_eq unfolds this definition, rewrites the two DOF equalities, and closes by norm_num to obtain the rational value $112$.
why it matters
Part 5 of the module: the Dirac-neutrino branch of the $g_\star$ ledger. Downstream g_star_dirac_eq pins the value at $112$; g_star_branch_gap shows the two conventions differ by $(7/8)\cdot 6 = 5.25$, so the neutrino choice is a real model input, not notation. FermionDOFGapBridge.n_generations_eq_D cites this branch when contrasting the minimal $g_f=90$ count against the Dirac $g_f=96$ alternative.
In the broader RS chain the gauge group and $D=3\Rightarrow 3$ generations are forced (T8 and ParticleGenerations); the $7/8$ weight and the Dirac-versus-minimal choice remain imported SM content. The definition therefore keeps the ledger honest: RS-sourced inputs are named, and the branch that moves $g_\star$ from $106.75$ to $112$ is isolated rather than hidden.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.