bosonic_dof
plain-language theorem explainer
Total bosonic relativistic degrees of freedom above the electroweak transition equal gluon plus symmetric-phase weak-boson plus Higgs counts. Cosmology and SM bookkeeping cite this as the integer g_b in g_★ = g_b + (7/8) g_f. The definition is a three-term sum of already-fixed sector counts; no proof beyond unfolding.
Claim. Define the total bosonic degree-of-freedom count above the electroweak scale by $g_b := g_{\mathrm{gluon}} + g_{W,B}^{\mathrm{sym}} + g_H$, where $g_{\mathrm{gluon}} = 8\times 2$, $g_{W,B}^{\mathrm{sym}} = 3\times 2 + 1\times 2$, and $g_H = 4$ (complex $SU(2)$ doublet counted in real components).
background
The module performs textbook high-temperature SM bookkeeping for $g_\star = g_b + (7/8)g_f = 106.75$, valid only for $T \gtrsim T_{\mathrm{EW}}$. RS supplies the gauge group $SU(3)\times SU(2)\times U(1)$ (from cube automorphisms) and three generations (from $D=3$); matter representations, the $7/8$ Fermi–Dirac weight, and the high-$T$ scope are imported physics.
Sector pieces used here: gluons are the $SU(3)$ adjoint times two massless polarizations; in the symmetric phase the weak sector is three $SU(2)$ generators plus one $U(1)$ hypercharge, each with two polarizations (total 8); the Higgs is one complex $SU(2)$ doublet, four real components. Parallel defs in Cosmology.GStarDerivation and FermionDOFGapBridge package the same 28 as gauge plus Higgs or gluon plus EW plus Higgs.
proof idea
Pure definition: a one-line natural-number sum of three prior defs (gluon_dof, weak_boson_dof_symmetric, higgs_dof). No tactics. The companion equality bosonic_dof_eq discharges the arithmetic to 28 by native_decide after unfolding.
why it matters
This is the bosonic half of the standard $g_\star = 106.75$ assembly. Downstream, bosonic_dof_eq locks the count at 28; Cosmology.GStarDerivation folds it into g_star_derived = bosonic_dof + (7/8)·fermionic_dof and proves equality to $427/4$, then packages the triple (bosonic 28, fermionic 90, formula) in GStarDerivationCert for the baryon-asymmetry bridge. Framework role is bookkeeping over RS-sourced gauge and generation inputs, not a novel RS mass or coupling prediction. It sits under the eight-tick / $D=3$ forcing chain only insofar as those fix the group and generation count used upstream of the fermion side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.