g_star_branch_gap
plain-language theorem explainer
The high-T Standard Model g_⋆ count with thermalized Dirac neutrinos exceeds the minimal (left-handed-only) neutrino branch by exactly 5.25. Cosmologists and RS auditors comparing the two neutrino conventions cite this gap. Proof rewrites both sides to the closed forms 112 and 106.75, then evaluates the difference by exact arithmetic.
Claim. In the high-temperature regime, the relativistic effective degree-of-freedom count with thermalized Dirac neutrinos minus the count under the minimal left-handed-only neutrino convention equals $5.25$, equivalently $\frac{7}{8}\cdot 6$.
background
This module performs textbook high-T Standard Model bookkeeping: $g_\star = g_b + (7/8) g_f$, valid only for $T \gtrsim T_{\mathrm{EW}}$ where every listed species is relativistic. The bosonic side is $g_b = 28$ (gluons, electroweak bosons, Higgs). The fermionic weight $7/8$ is the usual Fermi–Dirac to Bose–Einstein energy-density integral ratio; RS supplies the spin-statistics sign, not the integral value.
Two fermionic tallies are carried. The default (minimal-neutrino) branch takes left-handed neutrinos only, so $g_f = 90$ and $g_\star = 106.75 = 427/4$. The Dirac branch thermalizes right-handed partners as well, adding six fermionic degrees of freedom ($g_f = 96$) and yielding $g_\star = 112$. Upstream equalities pin both closed forms: the derived branch equals $106.75$, the Dirac branch equals $112$.
RS-sourced inputs to the count are the gauge group from cube automorphisms, three generations from $D=3$, and the FD/BE sign from the eight-tick spin-statistics theorem. Matter representations and the neutrino chirality convention remain imported SM content, not RS predictions.
proof idea
One short tactic proof. Rewrite the Dirac value via its closed-form equality to $112$, and the derived (minimal-neutrino) value via its closed-form equality to $106.75$. The goal collapses to the numerical identity $112 - 106.75 = 5.25$, discharged by norm_num. No unfolding of the underlying DOF sums is needed once those two equalities are in hand.
why it matters
The module header flags this whole file as BOOKKEEPING over adopted SM content, not a novel RS prediction. The gap theorem makes that honesty quantitative: switching the neutrino convention moves $g_\star$ by $(7/8)\cdot 6 = 5.25$, so the choice is a real model input, not cosmetic notation. Downstream consumers of either branch (threshold evolution in Cosmology.GStarThresholds, early-universe expansion rates) must pick a convention explicitly; this lemma records the exact offset between them.
Within the RS forcing chain the surrounding scaffolding still matters: gauge content from Q₃ automorphisms (GaugeFromCube), generation count $3$ from $D=3$ (ParticleGenerations / T8), and the FD/BE sign from the eight-tick spin-statistics theorem (T7). None of those force the neutrino chirality convention, which is why the two branches coexist and why their difference is stated as a proved identity rather than absorbed into a single derived constant. No downstream theorems currently depend on this gap; it is a local audit checkpoint inside the RelativisticDOF assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.