bosonic_dof
plain-language theorem explainer
Defines the total high-temperature bosonic relativistic degrees of freedom as the sum of gluon, electroweak gauge, and Higgs counts, equaling the standard SM value 28. Cosmology and SM DOF modules cite it when assembling g_*. It is a one-line arithmetic definition of three already-fixed natural-number pieces.
Claim. The total bosonic degree-of-freedom count is $N_b := N_{\mathrm{gluon}} + N_{\mathrm{EW}} + N_{\mathrm{Higgs}}$, with the standard high-$T$ SM values $16 + 8 + 4 = 28$.
background
This module records exact arithmetic identities that relate imported Standard Model relativistic DOF counts to $D=3$ combinatorial quantities (eight-tick period $2^D$, dimension gap). It does not derive the SM spectrum: gauge representations, the Higgs doublet, and the high-$T$ scope of $g_\star$ are imported physics; $D=3$ and the eight-tick structure are upstream RS results (T8 / DimensionForcing, EightTick).
Bosonic pieces used here: gluons contribute $8\times 2=16$ (adjoint of SU(3) times two transverse polarizations above $T_{\mathrm{EW}}$); unbroken EW bosons are written $2(D-1)^2$, which at $D=3$ is $8$ (four generators times two polarizations); the Higgs is one complex SU(2) doublet counted as $4$ real components. Parallel defs in StandardModel.RelativisticDOF and Cosmology.GStarDerivation use the same 28-count convention.
proof idea
Pure definition: unfold to the sum of three natural-number constants already fixed in-module (gluon_dof, ew_boson_dof, higgs_dof). No tactics or lemmas; the numerical identity $16+8+4=28$ is discharged downstream by decide after unfolding (e.g. bosonic_dof_eq).
why it matters
Supplies the bosonic half of the high-$T$ effective count $g_\star = N_b + (7/8)N_f$. Downstream, GStarDerivation uses it in g_star_derived, proves bosonic_dof = 28, and packages that fact in GStarDerivationCert for the baryon-asymmetry bridge. The module's assembled identity is $28 + (7/8)\times 90 = 106.75 = 427/4$.
Within RS, $D=3$ (T8) and the eight-tick octave justify the $D$-flavored rewritings of the EW and fermionic sides; the bosonic total itself remains the standard SM high-$T$ import. The honest split in the module doc still applies: this is kernel-checked bookkeeping, not a derivation of the gauge or Higgs content from the Recognition Composition Law or the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.