n_charged_leptons
plain-language theorem explainer
The number of charged lepton flavours is fixed at three (electron, muon, tau). Cosmology and running-coupling scorecards cite this constant when counting fermionic helicity states for high-T g_⋆ and for vacuum-polarization thresholds below M_Z. It is a bare natural-number definition, not a derived theorem.
Claim. The number of charged lepton flavours is $N_{\ell^{\pm}} = 3$ (electron, muon, and tau).
background
In the high-temperature Standard Model (above the electroweak transition) the relativistic effective degrees of freedom $g_\star$ are obtained by counting bosonic and fermionic helicity states. The module derives the textbook value $g_\star = 106.75 = 427/4$ from Q₃-forced SM content rather than inserting it by hand.
Fermionic counting splits into quarks, charged leptons, and neutrinos. Charged leptons contribute three flavours, each with two spin states and a particle/antiparticle pair, giving twelve degrees of freedom once the flavour count is multiplied through. The same integer appears in the alpha-running scorecard as the number of charged leptons that enter vacuum polarization below $M_Z$.
Sibling constants in the module fix the other SM multiplicities: three generations, three colours, two spin states, and two for particle/antiparticle.
proof idea
Bare definition equating the natural number of charged lepton flavours to 3. No tactics or lemmas; the value is the SM flavour count (e, μ, τ) recorded as a named constant for downstream arithmetic.
why it matters
Feeds the charged-lepton degree-of-freedom product (flavours × spins × particle/antiparticle) and the equality proof that this product equals 12. That count is unfolded inside the exact rational derivation $g_\star = 28 + (7/8)\cdot 90 = 427/4$, which replaces the hand-entered baryogenesis constant. The same integer is required by the alpha-running correction certificate (leptons field must equal 3). Within Recognition Science the three-flavour count is part of the Q₃ chord-cube particle content that forces the high-T $g_\star$ used in cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.