wboson
plain-language theorem explainer
Registers the charged weak bosons as a thermal species for the step-function g_*(T): mass threshold 402/5 GeV (≈80.4 GeV), six bosonic degrees of freedom (two charge states × three polarizations in the broken phase). Cosmologists citing the electroweak-sector species list use this entry. The body is a four-field structure literal; no proof obligations.
Claim. The $W^{\pm}$ bosons (broken electroweak phase) are the thermal species with name $\mathrm{W}^{\pm}$, mass threshold $m = 402/5\,\mathrm{GeV}$, internal degree count $g = 6$, and bosonic statistics.
background
The module builds the standard instantaneous-threshold model of $g_*(T)$: each species contributes its full relativistic DOF while $T$ exceeds its mass and drops out below it. Valid domain is $T \gtrsim 1,\mathrm{MeV}$; masses are PDG-rounded rationals used only for ordering against $T$.
A Species is a four-tuple: display name, mass threshold in GeV (rational), internal degree count, and a fermion flag. Below the electroweak scale the bosonic sector is counted in the broken phase (massive $W/Z$ with three polarizations, one physical Higgs). The $W^{\pm}$ entry encodes that broken-phase counting: two charge states times three polarizations gives six bosonic DOF, with $m \approx 80.4,\mathrm{GeV}$.
proof idea
Pure definition: the structure constructor is applied to the string $\mathrm{W}^{\pm}$, the rational mass $402/5$, the natural number $6$, and false (boson). No lemmas, tactics, or obligations.
why it matters
Feeds the electroweak-sector species list ew_species (top, Higgs, $Z$, $W^{\pm}$, bottom, tau, charm, muon, electron), which drives threshold decoupling in $g_(T)$ as temperature falls through the electroweak and GeV scales. The module answers the external-review gap that RS previously fixed a single $g_$ without a temperature-dependent function. Masses are imported thresholds only; RS $\varphi$-ladder mass modules predict them independently and are not re-derived here. Broken-phase $W/Z$ counting keeps the high-$T$ total aligned with the symmetric-phase bridge to RelativisticDOF.g_star_derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.