electron
plain-language theorem explainer
Registers the electron as a thermal species for the step-function g_*(T): mass threshold 0.000511 GeV, four internal degrees of freedom, fermionic statistics. Cosmology and early-universe bookkeeping cite it whenever e± drop out of the relativistic bath below the MeV scale. The body is a four-field structure literal; no proof obligations.
Claim. The electron is the thermal species with name "electron", mass threshold $m_e = 511/10^6$ GeV, internal degree count $g = 4$, and fermionic statistics (true).
background
The module builds the standard instantaneous-threshold model of $g_*(T)$, the effective number of relativistic degrees of freedom. Each species contributes its full DOF count while $T$ exceeds its mass and drops out below that threshold; the QCD switch at $T_{\mathrm{QCD}} \approx 0.15$ GeV replaces quark–gluon content by pions. All arithmetic is exact over $\mathbb{Q}$.
A thermal species is a four-tuple: display name, mass threshold in GeV (rational PDG-rounded approximation; only order relative to $T$ matters), internal DOF count, and a Boolean for Fermi vs Bose statistics. Fermions later enter $g_*$ with the usual $7/8$ weight.
Masses are imported ordering thresholds, not re-derived from the $\varphi$-ladder. Particle content matches the SM bookkeeping in RelativisticDOF. Valid domain is $T \gtrsim 1$ MeV (above neutrino decoupling); Boltzmann tails and the $(4/11)^{4/3}$ reheating factor are omitted by design.
proof idea
Pure definition: the structure constructor is applied to the four concrete fields "electron", 511/1000000, 4, and true. No lemmas, tactics, or obligations.
why it matters
Supplies the electron row in the species table that drives the step-function $g_*(T)$. Below the electron threshold the relativistic bath loses the $e^\pm$ contribution (4 fermionic DOF, weighted $7/8$), which is the last SM charged-lepton drop-out before neutrino decoupling and a standard textbook checkpoint the module proves as a spot check.
Downstream chemistry modules (electron affinity proxies, halogen/noble-gas closure, ionic-bond valence, ferromagnetism below the Curie point) reference electron bookkeeping in related RS chemistry layers; the cosmological definition anchors the shared SM particle identity. The module answers the external-review gap that RS previously fixed a single $g_*$ number without temperature-dependent thresholds. It does not touch the forcing chain T0–T8 or the Recognition Composition Law directly; it is applied SM content for cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.