higgs_dof_eq
plain-language theorem explainer
The Higgs relativistic DOF count equals 4 (one complex SU(2) doublet as four real components). Cited when assembling the high-T bosonic tally that enters g_*. Proof is a one-line native_decide check that the local definitional constant is 4.
Claim. The Higgs-sector degree-of-freedom count equals $4$: one complex $SU(2)$ doublet contributes four real components above the electroweak transition.
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=8$, dimension gap, generation count). Per the module status note, the SM matter representations, the minimal-neutrino convention, and the Fermi/Bose thermal weights are imported physics, not RS derivations; only the numerical identities among those counts are proved here.
Upstream, both StandardModel.RelativisticDOF and Cosmology.GStarDerivation fix the Higgs count as a definitional natural: one complex $SU(2)$ doublet, counted once in real components, gives $2\times 2=4$ DOF above the EW transition. The local higgs_dof in this bridge module is the same constant. The surrounding bosonic sum is the textbook high-$T$ split $16$ (gauge) $+8$ (gluons) $+4$ (Higgs) $=28$.
proof idea
One-line tactic proof: native_decide evaluates the definitional equality higgs_dof = 4 in the kernel. No lemmas are invoked; the declaration is a machine-checked restatement of the imported SM Higgs doublet count.
why it matters
Closes the Higgs leg of the high-$T$ bosonic DOF identity $16+8+4=28$ that the module assembles into the standard $g_=106.75$ arithmetic ($28+(7/8)\times 90$). The module explicitly does not claim an RS derivation of the Higgs doublet or of $g_$; after the 2026-06-25 rescope it only certifies kernel-checked identities on imported counts, citing T8 ($D=3$) and the eight-tick period only as ambient combinatorial context. No downstream users are wired yet; the natural parent is the total bosonic DOF sum that feeds the $g_*$ bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.