dilution_from_potential
plain-language theorem explainer
The neutrino-to-photon temperature ratio cubed equals 4/11 once the coupled plasma is a pressure potential with entropy density s = dP/dT, both sectors obey FRW continuity, and the usual e± annihilation boundary data hold. Cosmologists fixing g_*s or the η_B dynamical prefactor from Recognition structure would cite it. The proof glues global adiabaticity of the potential fluid to free-streaming of decoupled neutrinos, then applies the algebraic dilution lemma.
Claim. Let $P$ be a pressure potential with entropy density $s=dP/dT$, and let $\rho=Ts-P$ be the Legendre energy density. Suppose the coupled sector and a free-streaming neutrino sector each satisfy their FRW continuity equations, the non-vanishing side conditions on $T$, $a$, $T_\nu$, $T_\gamma$, and $\alpha_\nu$ hold, $s(T(t_1))$ equals the radiation entropy of a $g_B=2$, $g_F=4$ plasma at $T_1$, $s(T(t_2))$ equals that of a pure photon plasma at $T_\gamma$, and neutrinos share temperature $T_1$ at $t_1$. Then $(T_\nu(t_2)/T_\gamma)^3=4/11$.
background
In the grand-canonical ensemble at vanishing chemical potential a fluid is fixed by one thermodynamic potential: the pressure $P(T)$ (equivalently grand-potential density $\Omega=-P$). Entropy density is defined by $s=dP/dT$, and energy density by the Legendre transform $\rho=Ts-P$ (energyOf). Euler $Ts=\rho+P$ and Gibbs–Duhem $dP/dt=s,T'$ are then identities of that structure, not extra equilibrium postulates. The module therefore collapses the two named hypotheses of earlier FRW entropy conservation into the single structural claim that the coupled sector has a differentiable pressure potential.
potential_entropy_constant upgrades the local continuity identity to global adiabaticity: $s(T(t_1))a(t_1)^3=s(T(t_2))a(t_2)^3$. Independently, radiation_aT_constant records free streaming of a decoupled $\rho\propto T^4$ gas: $aT$ is constant between any two times once that sector's continuity equation holds. Boundary data are the standard e± annihilation bookkeeping: before annihilation the coupled plasma has bosonic dof 2 and fermionic dof 4; after, only photons remain; neutrinos share the pre-annihilation temperature and then redshift freely. Radiation entropy densities are those of NeutrinoDilution.radiationEntropy, built from the Bose/Fermi entropy integrals of RadiationEntropyRelation.
proof idea
Three short steps.
-
Apply
potential_entropy_constantto the coupled sector (pressure potential, $s=dP/dT$, FRW continuity). Rewrite the resulting comoving-entropy equality with the before/after boundary datahbeforeandhafterto obtainradiationEntropy 2 4 T₁ · a(t₁)³ = radiationEntropy 2 0 Tγ · a(t₂)³. -
Apply
EntropyConservationFRW.radiation_aT_constantto the neutrino sector (continuity of $\alpha_\nu T_\nu^4$). Rewrite with the shared-temperature hypothesis to get free streaming $a(t_2)T_\nu(t_2)=a(t_1)T_1$. -
Feed both identities into
NeutrinoDilution.dilution_from_entropy_conservation, which algebraically yields $(T_\nu/T_\gamma)^3=4/11$ from the radiation-entropy ratio $g_{*s}^{\rm before}/g_{*s}^{\rm after}=(2+4·7/8)/2=11/4$.
why it matters
Capstone of the GrandPotential module: the classical neutrino dilution factor is obtained from FRW continuity plus the existence of a pressure potential and boundary data alone. Euler and Gibbs–Duhem, which were explicit hypotheses in EntropyConservationFRW.dilution_from_frw, are discharged upstream as theorems of the Legendre structure (potential_euler, potential_gibbs_duhem), so they no longer appear in the hypothesis list.
The sole downstream consumer is gStarS_from_potential, the companion capstone that installs present-day entropy density $(2\pi^2/45)·(43/11)·T_\gamma^3$. That factor $43/11=2+(21/4)·(4/11)$ is exactly photons plus three neutrino species diluted by this theorem; it is the effective entropy dof entering the $\eta_B$ dynamical prefactor. Within Recognition cosmology the result therefore closes the thermodynamic side of the baryon-asymmetry bookkeeping without residual equilibrium postulates beyond local equilibrium itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.