higgs_dof
plain-language theorem explainer
Fixes the Higgs contribution to high-temperature relativistic degrees of freedom at four real scalar modes: one complex SU(2) doublet counted componentwise above the electroweak transition. Cosmology and SM DOF tallies cite it when assembling g_b = 28 and g_⋆ = 106.75. The body is a bare natural-number constant, not a derived equality.
Claim. The Higgs sector contributes $4$ real relativistic degrees of freedom above the electroweak phase transition: one complex $SU(2)$ doublet has two complex components, each with two real parts.
background
The module derives the standard high-$T$ value $g_\star = 106.75$ by explicit SM helicity counting rather than inserting the number by hand. Above the electroweak transition every SM species is relativistic and unsuppressed, so $g_\star = g_b + (7/8) g_f$ with bosonic and fermionic counts fixed by the particle content forced by the $Q_3$ chord-cube structure.
Bosonic counting splits into gauge and Higgs pieces. The gauge sector is $SU(3)\times SU(2)\times U(1)$: $8+3+1=12$ generators, each with two polarisations while $W$ and $Z$ remain massless, giving $24$ modes. The Higgs is the remaining scalar sector: one complex $SU(2)$ doublet.
Sibling modules record the same constant (plain $4$, or equivalently $2(D-1)$ with $D=3$). The present definition is the local copy used by the cosmology $g_\star$ derivation.
proof idea
No proof obligations. The declaration is a definitional abbreviation of the natural number $4$, matching the textbook real-component count of a complex $SU(2)$ doublet. Downstream equalities such as bosonic_dof_eq unfold this constant and discharge the arithmetic by decide.
why it matters
Without this four-mode Higgs piece the bosonic total would be $24$ rather than $28$, and the closed rational $g_\star = 427/4$ would fail. It feeds bosonic_dof ($\mathrm{gauge_dof}+\mathrm{higgs_dof}$), the certificate bosonic_dof_eq : bosonic_dof = 28, and the master identity g_star_derived_eq that recovers $106.75$. Parallel SM and unification modules reuse the same constant in their own bosonic tallies and in GStarCert.
In the broader Recognition chain the count is part of making the high-$T$ effective DOF a derived quantity tied to $Q_3$-forced SM content (three generations, $D=3$ spatial dimensions, eight-tick structure upstream), rather than a free cosmological input. It closes the gap between the hand-entered baryogenesis constant and the explicit particle ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.