g_star_derived
plain-language theorem explainer
The high-temperature SM effective relativistic DOF count is assembled as bosonic DOF plus (7/8) times fermionic DOF, equaling 106.75. Cosmology bridges and baryogenesis modules cite it as the fixed high-T value of g_star. The body is a one-line real combination of the local bosonic count, fermionic count, and Fermi–Dirac weight.
Claim. Define the high-$T$ effective relativistic degree-of-freedom count by $g_\star := g_b + \frac{7}{8}\, g_f \in \mathbb{R}$, where $g_b$ is the total bosonic DOF above the electroweak scale and $g_f$ is the total fermionic DOF (three generations). With the standard bookkeeping values $g_b = 28$ and $g_f = 90$, one has $g_\star = 106.75 = 427/4$.
background
This module performs textbook high-temperature Standard Model bookkeeping for the effective relativistic degree count $g_\star = g_b + (7/8) g_f$, valid only for $T \gtrsim T_{\mathrm{EW}}$. The STATUS TAG is explicit: bookkeeping over adopted SM content, not a novel RS prediction of a new number.
RS supplies three inputs proved upstream: the gauge group $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ from $Q_3$ automorphisms (GaugeFromCube), the generation count $3$ from face-pairs in $D=3$ (ParticleGenerations), and the Fermi–Dirac versus Bose–Einstein sign from the eight-tick spin-statistics theorem. Imported (not RS-derived) are the SM fermion representations, the minimal-neutrino convention (left-handed only, two DOF per generation), and the integral value $7/8$ of the Fermi–Dirac to Bose–Einstein energy-density ratio.
Locally, bosonic_dof sums gluons, symmetric-phase weak bosons, and the Higgs to $28$; fermionic_dof is three generations times thirty DOF per generation, totaling $90$; fermi_dirac_weight is the constant $7/8$.
proof idea
Definitional one-liner: cast the natural-number bosonic count to $\mathbb{R}$, cast the natural-number fermionic count to $\mathbb{R}$, multiply the latter by the real constant $7/8$, and add. No tactics, no lemmas, no unfolding beyond the three named ingredients. Numerical identity $28 + (7/8)\cdot 90 = 106.75$ is discharged downstream by separate equality theorems.
why it matters
This real-valued assembly is the StandardModel-side source for the high-$T$ constant used across cosmology. Downstream, Cosmology.GStarDerivation re-expresses the same combination as an exact rational $427/4$, proves decimal and baryogenesis bridges, and packages the three load-bearing facts (bosonic $28$, fermionic $90$, formula equals $427/4$) in GStarDerivationCert. GStarThresholds equates the high-$T$ evaluation of the temperature-dependent $g_\star(T)$ to this definition, so the old free-standing $106.75$ becomes a function value.
In the forcing chain it is consumed by T6T8_To_CosmologyConstants_Bridge, linking $\phi$-forced structure and $D=3$ to cosmological constants. The honest split matters: RS forces group, generation count, and statistics sign; the SM representation content and the $7/8$ integral remain imported. A Dirac-neutrino branch ($g_f=96$, $g_\star=112$) is acknowledged as an explicit model alternative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.