gElectron
plain-language theorem explainer
The electron–positron sector contributes four internal degrees of freedom: two spin states for each of e⁻ and e⁺. Cosmologists computing present-day g*s and the neutrino temperature dilution factor cite this MODEL input. It is a bare rational constant, not a derived theorem.
Claim. The internal degrees of freedom of the electron–positron pair equal $4$ (two spin states times particle and antiparticle). This is a fixed MODEL input from Standard Model particle content.
background
The module derives the entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in the narrow window $(7.0393, 7.0396)$, replacing a bare $7.04$ constant in the baryogenesis lane. Three ingredients enter: a proved $\zeta(3)$ window, a proved $\pi^4$ window, and the arithmetic identity $g_{*s}=43/11$ built from Standard Model particle content.
Present-day entropy degrees of freedom count photons (2 polarizations), residual neutrinos after $e^\pm$ annihilation, and the fermion weight $7/8$. Before annihilation the plasma also includes the electron–positron sector. The four internal dof of that sector are the quantity fixed here: two spin states for $e^-$ and two for $e^+$.
Sibling constants fix the photon ($g_\gamma=2$) and three neutrino generations ($g_\nu=6$). The combination $g_\text{before}=g_\gamma+(7/8)g_{e^\pm}$ then yields the pre-annihilation entropy dof $11/2$.
proof idea
Pure definitional assignment: the rational constant is set to $4$. No lemmas, tactics, or arithmetic are required. Downstream theorems unfold the name and discharge the resulting numeral by norm_num.
why it matters
Feeds three immediate consumers. gBefore builds the pre-annihilation plasma dof as $g_\gamma+(7/8)\cdot 4=11/2$. dilutionCubed_eq unfolds this constant (with $g_\text{after}$, fermion weight, and photon dof) to prove the classic dilution factor $(T_\nu/T_\gamma)^3=4/11$. In the NeutrinoDilution module, plasma_before_eq_gBefore identifies the functional-layer radiation entropy of a $2+4$ plasma with the same $11/2$ value, linking the arithmetic layer to the thermodynamic integrals.
Together these steps close the MODEL-input half of $g_{*s}=43/11$, which is the third pillar of the entropy-per-photon derivation used by the baryogenesis dynamical prefactor. The fermion weight $7/8$ itself is already theorem (from $\eta(4)=(7/8)\zeta(4)$ and the Fermi–Dirac integrals), so only the particle-content integers remain as MODEL data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.