bosonic_dof_eq
plain-language theorem explainer
Above the electroweak transition the Standard Model has exactly 28 bosonic helicity degrees of freedom: 12 massless gauge generators times 2 polarisations, plus 4 real Higgs components. Cosmology and SM counting modules cite this equality when assembling g_⋆ = 106.75. The proof unfolds the four natural-number definitions and closes by decide.
Claim. The total bosonic helicity count above the electroweak phase transition equals $28$: $$g_b = N_{\mathrm{gen}}\,N_{\mathrm{pol}} + N_{H} = (8+3+1)\cdot 2 + 4 = 28.$$
background
This module derives the high-temperature relativistic effective degrees of freedom $g_\star$ from explicit Standard Model particle content rather than a hand-entered constant. Above the electroweak transition every SM species is relativistic, and $g_\star = g_b + (7/8) g_f$ with the textbook value $28 + (7/8)\cdot 90 = 106.75$.
Bosonic counting splits into gauge and Higgs sectors. Gauge generators are the SM Lie-algebra dimension $8+3+1$ (gluons, $W^a$, hypercharge $B$). Each massless gauge boson contributes two transverse helicities, so gauge DOF equal $12\times 2$. The Higgs is one complex $SU(2)$ doublet, counted as four real scalar components. Total bosonic DOF is their sum.
The module works entirely in exact $\mathbb{N}$ and $\mathbb{Q}$ arithmetic; this lemma is the bosonic half of that count.
proof idea
Term-mode style via tactics: unfold bosonic_dof, gauge_dof, gauge_generators, gauge_polarisations, and higgs_dof to expose the ground terms $(8+3+1)\cdot 2 + 4$, then decide evaluates the closed natural-number expression to $28$. No external lemmas are required beyond definitional equality.
why it matters
This equality is the bosonic pillar of the derived $g_\star = 106.75$ chain. It is packaged into gStarDerivationCert (with the fermionic twin and the bridge back to the baryogenesis constant) and re-exported by StandardModel.RelativisticDOF for g_star_derived_eq, gStarCert, and the Dirac-neutrino variant. Downstream, bosonic_traces_to_Q3 and the FermionDOFGapBridge use it to tie the count to Q₃ chord-cube structure (SU(3) adjoint dimension 8, total $g_b = 28$). In the Recognition framework it converts the module-doc claim that Q₃-forced SM content fixes $g_b = 28$ into a machine-checked fact, closing the bosonic side of the exact rational $427/4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.