charged_lepton_dof_per_gen
plain-language theorem explainer
Charged leptons contribute four relativistic degrees of freedom per generation: one flavor times two chiralities times particle plus antiparticle. Anyone assembling the high-T Standard Model g_* count uses this factor when summing fermion DOF. The definition is the direct product of those three combinatorial inputs.
Claim. The relativistic degree-of-freedom count for charged leptons in one generation is $1 \times 2 \times 2 = 4$, namely one flavor, left and right chiralities, and particle plus antiparticle.
background
This module performs textbook high-temperature Standard Model bookkeeping for $g_\star = g_b + (7/8)g_f = 106.75$, valid only for $T \gtrsim T_{\mathrm{EW}}$ where every listed species is relativistic. Status is bookkeeping over adopted SM content, not a novel RS prediction.
Two local combinatorial factors enter the charged-lepton count: chiralities is fixed at 2 (left plus right), and particle_antiparticle is fixed at 2. The leading 1 is the single charged-lepton flavor per generation (e, μ, or τ).
RS supplies the gauge group and the generation count 3 upstream; the matter representations themselves (which reps the fermions occupy) are imported standard physics.
proof idea
Pure definition: the product of one flavor, the chirality factor 2, and the particle-antiparticle factor 2. No proof obligations. The companion equality theorem discharges the arithmetic to 4 by native_decide.
why it matters
This factor is the charged-lepton term in the per-generation fermion sum: quarks plus charged leptons plus neutrinos. That sum feeds both the minimal-neutrino branch (left-handed only) and the thermalized-Dirac-neutrino branch of the $g_\star$ assembly.
The companion equality pins the value at 4, so downstream rational arithmetic for $g_f$ and $g_\star = 427/4$ stays exact. Within the RS framing, generation count and gauge structure are RS-sourced; this DOF factor is ordinary SM representation content used as an input to that bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.