dilutionCubed_eq
plain-language theorem explainer
The cubed neutrino-to-photon temperature ratio after e± annihilation equals 4/11. Cosmologists cite this as the arithmetic content of entropy conservation in the photon–electron plasma while decoupled neutrinos free-stream. The proof unfolds the rational dof definitions and evaluates 2/(2+(7/8)·4) by norm_num.
Claim. The entropy-dilution ratio $g_{\mathrm{after}}/g_{\mathrm{before}}$ equals $4/11$, where $g_{\mathrm{after}}=2$ (photons only) and $g_{\mathrm{before}}=2+(7/8)\cdot 4=11/2$ (photons plus $e^{\pm}$ with fermionic weight $7/8$).
background
The module derives the present-day 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. One MODEL-arithmetic ingredient is the effective entropy degrees of freedom $g_{*s}$, which folds in neutrino dilution after electron–positron annihilation.
Photon internal dof are $g_\gamma=2$. Electron–positron internal dof are $g_{e}=4$. The fermionic entropy weight is the rational $7/8$, now theorem-backed by the identity $\eta(4)=(7/8)\zeta(4)$ and the matching thermodynamic integrals. Before annihilation the photon–electron plasma has $g_{\mathrm{before}}=2+(7/8)\cdot 4=11/2$; after annihilation only photons remain, so $g_{\mathrm{after}}=2$.
Entropy conservation in that sector ($g(aT)^3$ fixed) while decoupled neutrinos redshift freely forces $(T_\nu/T_\gamma)^3=g_{\mathrm{after}}/g_{\mathrm{before}}$. The definition dilutionCubed is exactly that rational quotient.
proof idea
Term-mode arithmetic. Unfold the definition of the dilution ratio as $g_{\mathrm{after}}/g_{\mathrm{before}}$, then the expressions $g_{\mathrm{after}}=g_\gamma$, $g_{\mathrm{before}}=g_\gamma+(7/8)g_e$, and the constants $g_\gamma=2$, $g_e=4$, fermion weight $7/8$. A single norm_num closes $2/(2+(7/8)\cdot 4)=4/11$ over the rationals.
why it matters
This is the arithmetic spine of the classical $4/11$ neutrino dilution factor inside the entropy-per-photon pipeline. Downstream, gStarS_eq rewrites present-day $g_{*s}$ as $43/11$ by substituting this identity into the combination of photons, weighted neutrinos, and the cubed dilution. Separately, NeutrinoDilution.dilution_eq_dilutionCubed proves provenance: the physically derived $(T_\nu/T_\gamma)^3$ from entropy conservation and free streaming equals this same rational, so the MODEL arithmetic and the conservation law agree.
In the module's three-ingredient story (ζ(3) window, π⁴ window, $g_{*s}=43/11$), this theorem discharges the pure-arithmetic half of ingredient 3. It does not itself invoke Recognition-Science forcing (T0–T8) or the J-cost; it is Standard-Model particle content plus Fermi–Dirac weight, packaged so the baryogenesis prefactor can cite a derived $s/n_\gamma$ band rather than a bare 7.04.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.