potential_entropy_conserved
plain-language theorem explainer
For a fluid whose pressure is a differentiable potential with entropy density s = dP/dT, the FRW continuity equation forces d/dt(s a³) = 0 at each time. Cosmologists tracking adiabatic expansion under local equilibrium at zero chemical potential would cite this. The proof is a term-mode feed of the derived Euler and Gibbs–Duhem identities into the general comoving-entropy theorem, so equilibrium structure alone discharges the prior hypotheses.
Claim. Let $P,s$ be functions of temperature and $T,a$ functions of time. Suppose $T(t)\neq 0$, $\mathrm{d}P/\mathrm{d}T$ at $T(t)$ equals $s(T(t))$, $s$ is differentiable at $T(t)$, and $T,a$ are differentiable at $t$. Write $\rho=T s-P$ for the Legendre energy density. If the FRW continuity equation holds as $a(t)\cdot(T(t)\,s'(T(t))\,T'(t))=-3 a'(t)(\rho+P)$ at $t$, then $\frac{d}{dt}\bigl(s(T(t))\,a(t)^3\bigr)=0$.
background
In the grand-canonical ensemble at zero 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=T\cdot s-P$ (energyOf).
The upstream theorem comoving_entropy_conserved already showed that FRW continuity $a\rho'=-3a'(\rho+p)$ forces $d/dt(s a^3)=0$, but only after assuming Euler $T s=\rho+p$ along the trajectory and Gibbs–Duhem $p'=s T'$ at the given time. This module derives both from the potential structure: Euler is the algebraic identity of the Legendre transform, and Gibbs–Duhem is the chain rule on $P\circ T$.
Thus the two named equilibrium postulates collapse into the single structural claim that pressure is a differentiable potential with $s=dP/dT$ — the definition of local equilibrium at $\mu=0$, not an extra dynamical assumption.
proof idea
Pure term proof: apply the upstream comoving_entropy_conserved after filling every hypothesis from the potential calculus.
- Energy derivative along the trajectory comes from
potential_energy_deriv(gives $\rho'=T\cdot s'\cdot T'$). - Pressure derivative is
potential_gibbs_duhem(chain rule: $p'=s(T)T'$). - Entropy derivative is
potential_entropy_deriv(chain rule on $s\circ T$). - Euler holds pointwise by the algebraic identity
potential_euler. - Scale-factor and temperature derivatives, the nonzero-temperature guard, and the continuity hypothesis
hcontare passed through unchanged.
No new calculus is done here; the work is wiring the derived identities into the general adiabatic-expansion theorem.
why it matters
This is the structural collapse the module advertises: comoving entropy conservation no longer needs independent Euler and Gibbs–Duhem postulates. One statement — pressure is a differentiable potential with $s=dP/dT$ — plus FRW continuity is enough.
Downstream, potential_entropy_constant globalizes the pointwise vanishing derivative: whenever the potential structure and continuity hold at every time, $s(T(t_1))a(t_1)^3=s(T(t_2))a(t_2)^3$. That global adiabaticity is the bookkeeping backbone for radiation-era entropy and for the concrete plasma realization later in the same module (Bose/Fermi log-kernel integrals giving $P\propto T^4$).
In the broader Recognition cosmology stack this closes the equilibrium side of the entropy-conservation chain without extra dynamical assumptions, leaving only continuity and the potential definition of local equilibrium.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.