bosonic_dof
plain-language theorem explainer
Defines the total bosonic helicity count above the electroweak transition as the sum of gauge-boson and Higgs degrees of freedom. Cosmologists deriving the high-T effective relativistic count g_⋆ cite it as the bosonic half of g_⋆ = g_b + (7/8) g_f. The body is a one-line sum of two already-defined natural numbers.
Claim. The total number of bosonic degrees of freedom above the electroweak phase transition is $g_b := g_{\mathrm{gauge}} + g_{\mathrm{Higgs}}$, where $g_{\mathrm{gauge}}$ is the gauge-boson count (generators times polarisations) and $g_{\mathrm{Higgs}} = 4$ for one complex $SU(2)$ doublet.
background
This module replaces the hand-entered constant $g_\star = 106.75$ used in baryon-asymmetry work by an explicit Standard Model helicity count above the electroweak transition. In that regime every SM species is relativistic and unsuppressed, so
$$g_\star = g_b + \tfrac78 g_f.$$
The gauge piece is forced by the $Q_3$ chord-cube content: $SU(3)\times SU(2)\times U(1)$ gives $8+3+1=12$ generators, each with two polarisations while $W$ and $Z$ remain massless, hence $g_{\mathrm{gauge}}=24$. The Higgs is one complex $SU(2)$ doublet, counted as four real scalar components. Their sum is the bosonic input to the rational formula $g_\star = 28 + (7/8)\cdot 90 = 427/4$.
proof idea
Pure definitional abbreviation: unfold to the sum of the two sibling naturals gauge_dof (generators times polarisations) and higgs_dof (the constant 4). No tactics, no lemmas. Downstream equality to 28 is discharged separately by unfolding those constituents and decide.
why it matters
Supplies the bosonic half of the derived $g_\star$. Immediate consumers are the equality theorem that pins the count at 28, the rational definition $g_\star^{\mathrm{der}} = g_b + (7/8)g_f$, its closed form $427/4$, and the certificate structure that bundles bosonic=28, fermionic=90, and the bridge back to the baryogenesis constant. Parallel SM relativistic-DOF modules reuse the same total. Within Recognition Science this is the concrete particle-content step that turns the high-T effective count from a fitted input into Q₃-forced arithmetic, feeding any cosmology that needs $g_\star$ (baryon asymmetry, freeze-out rates).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.