dilutionCubed
plain-language theorem explainer
Defines the cubed neutrino-to-photon temperature ratio as the rational quotient of post- to pre-annihilation entropy degrees of freedom in the photon–electron sector. Cosmologists cite it as the arithmetic stand-in for (T_ν/T_γ)³ before the equality to 4/11 is proved. The body is a one-line ratio of the two g-factors already fixed by SM particle content.
Claim. The cubed dilution factor is the rational $g_{\mathrm{after}}/g_{\mathrm{before}}$, where $g_{\mathrm{after}}$ is the entropy dof of the photon sector alone and $g_{\mathrm{before}}$ is the entropy dof of the photon–electron plasma before $e^{\pm}$ annihilation.
background
The EntropyPerPhoton module derives the present-day entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ used in the baryogenesis lane, replacing a bare 7.04 constant. One arithmetic ingredient is $g_{*s}=43/11$, which folds in neutrino dilution after $e^{\pm}$ annihilation.
Before annihilation the coupled plasma has entropy dof $g_{\mathrm{before}}=g_\gamma+(7/8)g_{e^{\pm}}=2+(7/8)\cdot 4=11/2$. After annihilation only photons remain, so $g_{\mathrm{after}}=g_\gamma=2$. Entropy conservation keeps $g(aT)^3$ fixed in the coupled sector while decoupled neutrinos free-stream, forcing $(T_\nu/T_\gamma)^3$ equal to that dof ratio.
The fermion weight $7/8$ is not a model input here: it is proved from the Fermi–Dirac integrals in Cosmology.FermionWeight and FermionWeightIntegral.
proof idea
Pure definition: the body is the rational quotient gAfter / gBefore. No tactics or lemmas. Unfolding later (in dilutionCubed_eq) substitutes gAfter = gPhoton = 2 and gBefore = gPhoton + fermionWeight * gElectron = 2 + (7/8)·4, then norm_num yields $4/11$.
why it matters
This rational is the bridge between SM particle counting and the physical neutrino dilution theorem. Downstream, dilutionCubed_eq proves the value is exactly $4/11$; gStarS inserts it into present-day entropy dof as $g_\gamma+(7/8)g_\nu\cdot\mathrm{dilutionCubed}$.
In NeutrinoDilution, dilution_eq_dilutionCubed identifies the physically derived $(T_\nu/T_\gamma)^3$ (from entropy conservation plus free streaming) with this arithmetic definition, and dilution_from_entropy_conservation concludes $(T_\nu/T_\gamma)^3=4/11$. The module doc ties the result into $g_{*s}=43/11$ and the $s/n_\gamma\in(7.0393,7.0396)$ window for baryogenesis.
No Recognition forcing-chain landmark (T0–T8) is touched directly; the declaration is Standard-Model cosmology arithmetic feeding the entropy-per-photon derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.