charged_lepton_dof_per_gen_eq
plain-language theorem explainer
Charged leptons contribute exactly four relativistic degrees of freedom per generation: one flavor, both chiralities, particle and antiparticle. Anyone assembling the high-T SM fermion count g_f cites this equality. The proof is a one-line native_decide on the product definition.
Claim. The charged-lepton relativistic degree-of-freedom count per generation equals $4$, i.e. $1 \times 2 \times 2 = 4$ (one flavor, two chiralities, 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}}$. Status is explicit: correct arithmetic over adopted SM content, not a novel RS prediction.
RS supplies the gauge group from cube automorphisms, three generations from $D=3$, and the Fermi/Bose sign via spin-statistics. Matter representations and the thermal weight $7/8$ are imported physics.
The upstream definition sets charged-lepton DOF per generation to $1 \times$ chiralities $\times$ particle_antiparticle, documented as "1 flavor × 2 chiralities × 2 (p + ap) = 4." Neutrinos are counted separately under the minimal left-handed-only convention (2 DOF per generation).
proof idea
Term-mode proof by native_decide. The definition is a pure natural-number product of fixed constants (one flavor, two chiralities, particle plus antiparticle). Kernel evaluation reduces the product to 4 with no lemmas or case splits.
why it matters
Fills one additive slot in the fermion side of the $g_\star$ ledger: three generations of charged leptons contribute $3 \times 4 = 12$ to $g_f$ before the $7/8$ weight. The module status tag marks this as BOOKKEEPING over adopted SM content.
No downstream dependents are recorded in the graph for this equality itself; it exists so the assembled $g_f$ and $g_\star$ theorems can quote a named, proved constant rather than an inline numeral. Framework landmarks touched only indirectly: generation count 3 from $D=3$ (ParticleGenerations) and gauge structure from GaugeFromCube enter the larger assembly, not this local product.
Does not address the Dirac-neutrino branch ($g_f=96$, $g_\star=112$) or temperature-dependent decoupling (Cosmology.GStarThresholds).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.