n_charged_leptons
plain-language theorem explainer
The number of charged lepton flavors (e, μ, τ) that enter vacuum polarization below the Z pole is fixed at three. Alpha-running scorecards and early-universe g⋆ counts cite this constant so particle content is not a free parameter. The body is a bare natural-number assignment.
Claim. The number of charged lepton flavors contributing to vacuum polarization below $M_Z$ equals $3$.
background
The module treats the QED running of the fine-structure constant from $q^2=0$ to $q^2=M_Z^2$ as the dominant radiative correction to electroweak mass predictions. RS forces $\alpha^{-1}(0)\in(137.030,137.039)$; PDG $\alpha^{-1}(M_Z)\approx127.951$ then implies a running ratio in $(0.933,0.935)$. That ratio is fixed by the 1-loop vacuum-polarization sum over species below $M_Z$:
$\Delta\alpha=\alpha/(3\pi)\sum_f N_c Q_f^2[\log(M_Z^2/m_f^2)-5/3]$.
The charged-lepton term in that sum needs a flavor count. The same integer appears in the cosmology module as the charged-lepton flavor count (e, μ, τ), feeding fermionic degrees of freedom for $g_\star$.
proof idea
Pure definition: the natural number is assigned the value 3. No tactics, no lemmas, no computation.
why it matters
Locks the lepton half of the "zero free parameters" claim on the alpha-running scorecard: the certificate structure requires n_charged_leptons = 3 alongside five light quarks and the running-ratio band. Downstream, cosmology multiplies this by spin and particle/antiparticle factors to get charged-lepton DOF $=12$, which enters the closed-form $g_\star=427/4$. Together with the RS $\alpha^{-1}(0)$ band from the forcing chain, the fixed particle content makes the $M_Z$ correction calculable rather than fitted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.