gauge_dof
plain-language theorem explainer
Counts massless Standard Model gauge-boson helicity states above the electroweak transition as twelve generators times two transverse polarisations, giving 24. Cosmologists deriving the high-T effective DOF g_⋆ cite this as the gauge piece of the bosonic total. The definition is a one-line product of the generator and polarisation counts.
Claim. The total number of gauge-boson degrees of freedom above the electroweak phase transition is $N_{\mathrm{gauge}} = N_{\mathrm{gen}} \times N_{\mathrm{pol}}$, where $N_{\mathrm{gen}} = 8+3+1$ (gluons, $W^a$, hypercharge $B$) and each massless gauge boson contributes $N_{\mathrm{pol}} = 2$ transverse helicities.
background
This module derives the high-temperature relativistic effective degrees of freedom $g_\star = 106.75$ by explicit Standard Model helicity counting rather than inserting the textbook constant by hand. Above the electroweak transition every SM species is relativistic and massless gauge bosons retain only transverse modes.
The gauge sector is fixed by the $Q_3$-forced group structure $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$: eight gluons, three weak bosons, and one hypercharge boson, for twelve generators. Each massless vector contributes two helicity states. The product is the gauge contribution to the bosonic count that later combines with the four real Higgs components to give $g_b = 28$.
Upstream, gauge_generators is defined as $8+3+1$ and gauge_polarisations as $2$; both are pure natural-number constants with no further hypotheses.
proof idea
Pure definitional abbreviation: multiply the generator count by the polarisation count. No tactics, no lemmas, no arithmetic beyond the product of two previously defined naturals.
why it matters
Supplies the gauge half of the bosonic DOF that feed bosonic_dof and the equality bosonic_dof_eq : bosonic_dof = 28. That bosonic total is unfolded inside g_star_derived_eq, which closes $g_\star = 28 + (7/8)\cdot 90 = 427/4$.
In the Recognition framework the particle content itself is forced by the $Q_3$ chord-cube structure (eight-tick octave, three spatial dimensions). Making the gauge count an explicit product rather than a magic number lets the derived $g_\star$ match the hand-entered baryogenesis constant by exact rational arithmetic, with a single native_decide at the end of the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.