comoving_entropy_conserved
plain-language theorem explainer
For a fluid in local equilibrium (Euler Ts=ρ+p and Gibbs–Duhem p′=sT′), the FRW continuity equation forces the comoving entropy density s a³ to have vanishing time derivative. Cosmologists deriving adiabatic expansion or neutrino dilution cite this in place of the usual postulate. The proof differentiates Euler, cancels T′ via Gibbs–Duhem, then combines continuity with T≠0 to show the product rule for s a³ is zero.
Claim. Let $\rho,p,s,T,a:\mathbb{R}\to\mathbb{R}$ be differentiable at $t$, with $T(t)\neq 0$. Suppose the Euler relation $T(u)s(u)=\rho(u)+p(u)$ holds for all $u$, Gibbs–Duhem $p'=s(t)T'$ holds at $t$, and FRW continuity $a(t)\rho'=-3a'(\rho(t)+p(t))$ holds at $t$. Then $\frac{d}{dt}(s\,a^3)\big|_{t}=0$.
background
This module sits in the cosmology layer that discharges two model hypotheses previously assumed in neutrino dilution: adiabatic expansion (comoving entropy $s a^3$ conserved) and free-streaming redshift ($a T$ constant for decoupled radiation). Both are derived here from FRW dynamics plus local equilibrium, with zero sorry.
Local equilibrium at vanishing chemical potential is encoded by the Euler identity $T s=\rho+p$ along the trajectory and the Gibbs–Duhem relation $p'=s T'$ at the evaluation time. Continuity $a\rho'=-3a'(\rho+p)$ is not an independent axiom in this development: the sibling result continuity_from_friedmann obtains it from the two Friedmann equations by differentiation and cancellation, i.e. Bianchi compatibility of Einstein's equations in FRW form.
The present theorem is the pointwise adiabatic step (§1 of the module). Global constancy $s(t_1)a(t_1)^3=s(t_2)a(t_2)^3$ is upgraded later via the mean-value theorem once the derivative vanishes everywhere.
proof idea
Differentiate the Euler identity with the product rule to get $T's+Ts'=\rho'+p'$, using uniqueness of derivatives after rewriting the two sides as equal functions. Add Gibbs–Duhem $p'=s T'$ via linear_combination to cancel the $T'$ terms, leaving $T s'=\rho'$.
Form $T(a s'+3 a' s)$ by combining $a\cdot(T s')$ with $3 a'\cdot$(Euler) and continuity; the combination is identically zero. Since $T(t)\neq 0$, cancel $T$ with mul_eq_zero to obtain the key identity $a s'+3 a' s=0$.
Finally apply the product and power rules: derivative of $s a^3$ is $s' a^3+s\cdot 3 a^2 a'$, which is $a^2$ times the key identity, hence zero. Rewrite the product derivative at that zero value.
why it matters
Comoving entropy conservation is the standard adiabatic postulate of early-universe thermodynamics; here it is a theorem from FRW continuity plus equilibrium identities. Downstream, comoving_entropy_constant lifts the pointwise vanishing derivative to equality of $s a^3$ at any two times, and entropy_conserved_from_friedmann composes this with continuity-from-Friedmann so that Friedmann I+II alone (plus equilibrium) yield adiabaticity without assuming continuity.
In GrandPotential, potential_entropy_conserved strengthens the hypotheses further: Euler and Gibbs–Duhem are derived from a pressure potential with $s=dP/dT$, then this theorem is applied. That closes the chain from a thermodynamic potential to adiabatic expansion.
Within the broader Recognition Science cosmology stack, the result discharges the adiabatic half of the former NeutrinoDilution model interface ($(T_\nu/T_\gamma)^3=4/11$ and $g_{*s}=43/11$), converting assumed conservation laws into FRW theorems. It is classical continuum thermodynamics, not a T0–T8 forcing step, but it is the bridge that lets RS cosmology inherit standard entropy bookkeeping without extra postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.