gNeutrino
plain-language theorem explainer
Neutrino internal degrees of freedom are fixed at the rational value 6: three generations, each with neutrino and antineutrino, each with one helicity. Cosmologists computing present-day entropy effective degrees of freedom g*s cite this MODEL census input. The declaration is a plain rational constant, not a derived identity.
Claim. The neutrino internal degree-of-freedom count is the rational $g_\nu = 6$, obtained as $3$ generations $\times$ $(\nu + \bar{\nu})$ $\times$ $1$ helicity (a Standard Model particle-content input).
background
The EntropyPerPhoton module derives the entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in a narrow window around 7.04, for use in the baryogenesis dynamical 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 species counts.
Present-day entropy degrees of freedom combine photons (2 polarizations) with fermionic species weighted by the Fermi–Dirac factor $7/8$. That weight is no longer a free MODEL constant: fermionWeight_eq_eta_zeta_ratio identifies it with $\eta(4)/\zeta(4)$, and fermi_integral_eq_weight_mul_bose matches the thermodynamic integrals $\int t^3/(e^t+1) = (7/8)\int t^3/(e^t-1)$. What remains MODEL is the relativistic-species census itself.
Neutrinos enter that census after $e^\pm$ annihilation, diluted by $(T_\nu/T_\gamma)^3 = 4/11$. Their raw internal count is this constant.
proof idea
Plain definition: the rational literal 6. No tactics, no lemmas. The value encodes the MODEL counting rule stated in the doc-comment (three generations, particle plus antiparticle, one helicity each). Downstream arithmetic unfolds this name and reduces by norm_num.
why it matters
Feeds the present-day entropy dof definition $g_{*s} = g_\gamma + (7/8), g_\nu, (4/11)$ and the theorem that evaluates it to $43/11$. Without a fixed neutrino count, the arithmetic closure of $g_{*s}$ (and thus the derived $s/n_\gamma$ band replacing the bare 7.04 prefactor) cannot fire.
In the module's status language this is MODEL particle content, not a Recognition forcing step: the framework landmarks T5–T8 and the RCL fix $J$, $\varphi$, the eight-tick period, and $D=3$, but do not by themselves enumerate SM generations or helicities. The declaration therefore pins the census input that the theorem-backed $7/8$ weight multiplies, keeping MODEL and THEOREM layers cleanly separated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.