ew_boson_dof
plain-language theorem explainer
Defines the unbroken-phase electroweak gauge-boson degree-of-freedom count as 2(D−1)², which evaluates to 8 when D=3. Anyone assembling the high-T SM bosonic tally (gluons + EW + Higgs) cites this bookkeeping constant. The body is a one-line arithmetic definition, not a derivation of the gauge content.
Claim. The electroweak gauge-boson DOF count in the unbroken phase is $2(D-1)^2$, where $D=3$ is the forced spatial dimension. Equivalently, four generators of $\mathrm{SU}(2)\times\mathrm{U}(1)$ each contribute two transverse polarizations, giving 8.
background
This module records exact arithmetic identities that rewrite imported Standard Model high-temperature degree-of-freedom counts in D-flavored notation. It does not derive the SM spectrum: gauge representations, the Higgs doublet, and thermal weights are imported physics; only the numerical re-expressions are kernel-checked here.
The sole parameter is $D$, fixed to 3 by the dimension-forcing step (T8). With that value, $(D-1)^2=4$ matches the generator count of $\mathrm{SU}(2)\times\mathrm{U}(1)$ above the electroweak scale, and the prefactor 2 encodes the two transverse polarizations of massless vector bosons.
Upstream, $D$ is the same constant appearing in AlphaDerivation and GapDerivation; locally it is re-exported so the bridge identities stay self-contained.
proof idea
There is no proof obligation: the declaration is a bare natural-number definition equal to $2((D-1)^2)$. Instantiating $D=3$ yields $2\cdot 4=8$ by ordinary arithmetic, discharged downstream by native_decide in the equality lemma that pins the constant to 8.
why it matters
Feeds the total bosonic DOF sum (gluons + electroweak + Higgs = 28) used in the assembled high-T identity $28+(7/8)\times 90=106.75$. The companion equality theorem records that the D-flavored form equals the textbook count 8.
In the Recognition framework this sits under Unification bookkeeping tied to T8 ($D=3$) and the eight-tick cadence $2^D=8$. It is deliberately scoped as imported SM content rewritten after the fact, not an RS derivation of electroweak gauge structure. Closing a true derivation would require forcing $\mathrm{SU}(2)\times\mathrm{U}(1)$ and the polarization count from RS premises, which this module explicitly does not claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.