bosonic_dof_eq
plain-language theorem explainer
The total bosonic relativistic degrees of freedom above the electroweak scale equal 28. Cosmologists and RS bridge authors cite this when assembling the textbook high-T count g_* = 106.75 from gauge plus Higgs content. The proof is a one-line native decision of the closed natural-number definition (gluons, electroweak vectors, and Higgs).
Claim. The total number of bosonic relativistic degrees of freedom in the high-temperature Standard Model (gauge bosons plus Higgs) equals $28$.
background
This module performs exact rational bookkeeping for the standard high-temperature relativistic effective count
$$g_\star = g_b + \tfrac78 g_f = 28 + \tfrac78\cdot 90 = 106.75,$$
valid only for $T\gtrsim T_{\mathrm{EW}}$ where every listed species is relativistic. The module status is honest bookkeeping over adopted SM content, not a novel RS prediction.
Locally, the bosonic total is the sum of gauge and Higgs pieces: eight gluons with two helicities each (16), the four massless electroweak vectors above the phase transition with two helicities each (8), and four real Higgs scalars from the complex doublet, giving $16+8+4=28$. Upstream RS inputs that feed the surrounding assembly are the gauge group from $Q_3$ cube automorphisms and the generation count $3$ from $D=3$; the representation content and the $7/8$ thermal weight remain standard physics imports.
proof idea
One-line computational proof. The tactic native_decide evaluates the closed natural-number definition of the bosonic total (assembled from the sibling gluon, weak-boson, and Higgs counts) and checks equality with $28$. No algebraic lemmas are required beyond decidable arithmetic on $\mathbb{N}$.
why it matters
This equality is the bosonic half of the $g_\star=106.75$ certificate. Downstream it is rewritten into g_star_derived_eq and g_star_dirac_eq, packed into gStarCert and the cosmology gStarDerivationCert, and exposed in bosonic_traces_to_Q3 so each bosonic slot can be tied back to $Q_3$ adjoint structure (eight gluons from $\mathrm{SU}(3)$). The Unification fermion-gap bridge reuses the same fact when comparing bosonic and fermionic ladders. Framework landmarks in play are the RS-sourced gauge group and $D=3$ generation count; the lemma itself only locks the arithmetic identity $g_b=28$ that those inputs feed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.