charged_lepton_dof
plain-language theorem explainer
Charged-lepton helicity states at high T equal three flavours times two spins times particle and antiparticle, giving twelve. Anyone assembling the SM fermionic count for g_⋆ cites this multiplicity. The body is the plain product of those three natural-number constants.
Claim. The charged-lepton contribution to relativistic degrees of freedom is $N_{\ell^{\pm}} = 3 \times 2 \times 2$, i.e. three flavours ($e,\mu,\tau$), both helicities, and particle plus antiparticle.
background
This module derives the high-temperature effective count $g_\star$ from explicit Standard Model helicity arithmetic rather than a hand-entered constant. Above the electroweak transition every SM species is relativistic, so $g_\star = g_b + (7/8)g_f$ with $g_b = 28$ and $g_f = 90$, yielding the exact rational $427/4 = 106.75$.
Fermion multiplicities factor into flavours, colours (for quarks), spin/helicity states, and particle versus antiparticle. For charged leptons the flavour count is three ($e,\mu,\tau$), both helicities are kept in the above-EW Dirac counting ($n_{\mathrm{spin}} = 2$), and particle plus antiparticle contributes a factor of two. Neutrinos are treated separately with a single helicity each under the minimal-SM convention.
proof idea
Pure definition: the natural number is the product of the three sibling constants (charged-lepton flavours, spin states, particle/antiparticle). No tactic proof; downstream equality lemmas unfold the product and close by decide.
why it matters
The count is the charged-lepton term inside total fermionic DOF (quarks plus charged leptons plus neutrinos). That sum feeds the derived $g_\star$ identity $g_\star = 28 + (7/8)\cdot 90 = 427/4$, which bridges to the existing baryogenesis constant. Module narrative ties the particle content to Q₃-forced SM structure; this definition supplies the twelve charged-lepton states in that forced tally.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.