g_star_dirac_high
plain-language theorem explainer
At high temperature ($T=200$ GeV), the instantaneous-threshold relativistic DOF count with thermalized right-handed Dirac neutrinos equals 112, not the minimal-SM 106.75. Cosmologists checking the Dirac branch of $g_*(T)$ against static SM bookkeeping would cite this. The proof is a one-line native rational decision over the active-species sum.
Claim. With thermalized right-handed Dirac neutrinos (3 generations, 12 fermionic degrees of freedom), the step-function relativistic count satisfies $g_*(T=200\,\mathrm{GeV})=112$.
background
The module builds the standard instantaneous-threshold model of $g_*(T)$: each SM species contributes its full relativistic weight while $T$ exceeds its mass threshold and drops out below it, with a QCD confinement switch near $0.15$ GeV. All sums are exact over $\mathbb{Q}$. Valid domain is $T\gtrsim 1$ MeV (above neutrino decoupling); Boltzmann tails, lattice QCD EOS, and the $(4/11)^{4/3}$ reheating factor are out of scope.
The parameterized count $g_*$ with an explicit neutrino sector sums per-species weights over species still active at $T$. The Dirac branch is the species with 12 DOF (3 gen $\times$ 4), versus the minimal-SM Majorana convention. High $T$ here means above every mass threshold (200 GeV sits above the top).
Mass thresholds are imported PDG-rounded cutoffs used only for ordering; particle content and the $7/8$ fermionic integral match the static RelativisticDOF bookkeeping.
proof idea
One-line computational proof. native_decide evaluates the finite rational sum that defines the Dirac-parameterized $g_*$ at $T=200$ and checks equality with 112. No intermediate lemmas are invoked beyond the definitions of the active-species filter and the per-species degree weights.
why it matters
Fills the high-$T$ Dirac spot check stated in the module header and doc-comment: with thermalized RH Dirac neutrinos the count is 112, matching the static bridge RelativisticDOF.g_star_dirac_eq. The neutrino convention is an honest external input; the two branches differ only through the neutrino term, by $(7/8)\cdot 6=5.25$ at high $T$.
No downstream theorems currently depend on this result. It is a machine-checked textbook calibration point for the cosmology $g_*(T)$ stack built to answer the external review that the repository lacked temperature-dependent DOF. It lives in the imported SM-content layer, not in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.