dilution_from_frw
plain-language theorem explainer
Under FRW continuity plus local equilibrium (Euler and Gibbs–Duhem) for the coupled plasma, and free-radiation continuity for decoupled neutrinos, the neutrino-to-photon temperature cube is forced to 4/11. Cosmologists deriving g*s or η_B prefactors from dynamics rather than model postulates would cite this. The proof derives global adiabaticity and free-streaming constancy, then hands both to the existing dilution algebra.
Claim. Let $\rho,p,s,T,a,T_\nu$ be differentiable real functions of time. Assume local equilibrium $T s=\rho+p$ and Gibbs–Duhem $p'=s T'$, the FRW continuity equation $a\rho'=-3a'(\rho+p)$ for the coupled sector, and free-radiation continuity for $\rho_\nu=\alpha_\nu T_\nu^4$. If before $e^\pm$ annihilation the entropy density is that of a $g_B=2$, $g_F=4$ plasma at shared temperature $T_1$, and after annihilation it is pure photons at $T_\gamma$, then $(T_\nu(t_2)/T_\gamma)^3=4/11$.
background
This module discharges the two MODEL hypotheses that NeutrinoDilution treated as inputs: adiabatic expansion of the coupled photon–$e^\pm$ sector, and free streaming of decoupled neutrinos. Both are derived from FRW continuity plus equilibrium identities, with no sorry.
Comoving entropy conservation says $s(t_1)a(t_1)^3=s(t_2)a(t_2)^3$ for any equilibrium fluid obeying continuity (Euler $T s=\rho+p$ at zero chemical potential, Gibbs–Duhem $p'=s T'$). Free streaming says $a T$ is constant for a decoupled radiation gas $\rho=\alpha T^4$ under its own continuity equation. Entropy density of a relativistic plasma is radiationEntropy gB gF T, built from Bose/Fermi entropy integrals; the boundary data here are $g_B{+}g_F: 2{+}4\to 2$ across $e^\pm$ annihilation with shared temperature at decoupling.
Upstream, comoving_entropy_constant and radiation_aT_constant upgrade pointwise vanishing derivatives to two-time equalities. dilution_from_entropy_conservation then turns those equalities into $(T_\nu/T_\gamma)^3=4/11$.
proof idea
Three steps. First apply comoving_entropy_constant on the coupled sector (using Euler, Gibbs–Duhem, and FRW continuity) between $t_1$ and $t_2$; rewrite the endpoint entropies via the before/after boundary hypotheses to get
$\mathrm{radiationEntropy},2,4,T_1\cdot a(t_1)^3=\mathrm{radiationEntropy},2,0,T_\gamma\cdot a(t_2)^3$.
Second apply radiation_aT_constant on the neutrino sector (free-radiation continuity for $\alpha_\nu T_\nu^4$), and use the shared-temperature hypothesis $T_\nu(t_1)=T_1$, to obtain $a(t_2)T_\nu(t_2)=a(t_1)T_1$.
Third feed both identities into NeutrinoDilution.dilution_from_entropy_conservation, which performs the pure algebraic reduction to $(T_\nu/T_\gamma)^3=4/11$.
why it matters
Capstone of the FRW entropy module: the classical neutrino dilution factor is no longer a model input but a theorem of continuity plus equilibrium. Downstream, gStarS_from_frw uses the same physics package to force present-day entropy density equal to $(2\pi^2/45)\cdot g_{*s}\cdot T_\gamma^3$ with $g_{*s}=43/11$, so the effective entropy dof in the $\eta_B$ dynamical prefactor is fixed by the continuity equations.
The sibling chain (§0–§3) already derives continuity from the two Friedmann equations and upgrades local conservation laws to global constancy; this theorem is the place those pieces land on the standard $4/11$ number. It sits in the cosmology layer that feeds baryon-asymmetry and photon-entropy bookkeeping, not in the T0–T8 forcing chain itself, but it removes two free hypotheses between FRW dynamics and the dilution cube used throughout RS cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.