potential_energy_deriv
plain-language theorem explainer
Along a temperature trajectory T(t), the energy density of a zero-μ potential fluid satisfies d/dt ρ(T(t)) = T(t)·s′(T(t))·T′(t). Cosmologists deriving adiabatic FRW expansion from the grand potential alone cite this chain-rule step. The proof composes the fundamental relation ρ′(T)=T·s′ with the trajectory derivative via HasDerivAt.comp.
Claim. Let $P,s,T:\mathbb{R}\to\mathbb{R}$ with energy density $\rho(x)=x\,s(x)-P(x)$. If $P'(T(t))=s(T(t))$, $s'(T(t))=s_T$, and $T'(t)=T'$, then $\frac{d}{dt}\rho(T(t))=T(t)\,s_T\,T'$ at time $t$.
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 is the Legendre transform $\rho=T,s-P$ (energyOf).
The module discharges the two equilibrium identities that EntropyConservationFRW.comoving_entropy_conserved previously took as hypotheses. Euler $T,s=\rho+P$ is algebraic in the Legendre transform (potential_euler). Gibbs–Duhem along a trajectory is the chain rule on $s=dP/dT$ (potential_gibbs_duhem). Differentiating $\rho=T,s-P$ then yields the fundamental relation $\rho'(T)=T,s'(T)$ (energy_deriv).
The present statement lifts that $T$-derivative to an arbitrary differentiable temperature path $T(t)$, which is the form needed when feeding FRW continuity in cosmic time.
proof idea
One short composition. First apply energy_deriv at the point $x=T(t)$ with the given $P$- and $s$-derivatives to obtain
$\mathrm{HasDerivAt},(\mathrm{energyOf},P,s),(T(t),s_T),(T(t))$.
Then compose with the trajectory derivative $hT$ via HasDerivAt.comp, and tidy with simpa on Function.comp and mul_assoc to rearrange the product $T(t),s_T,T'$.
why it matters
This is the time-domain form of $d\rho=T,ds$ required by the parent theorem potential_entropy_conserved. That result states that once pressure is a differentiable potential with $s=dP/dT$ (local equilibrium at $\mu=0$), FRW continuity alone forces $d/dt(s,a^3)=0$; Euler and Gibbs–Duhem are derived rather than assumed.
Together with potential_euler, potential_gibbs_duhem, and energy_deriv, the lemma collapses the two named hypotheses of comoving_entropy_conserved into a single structural statement about the grand potential. Downstream the same structure is realized by the massless Bose/Fermi plasma pressure $P\propto(g_B+(7/8)g_F)T^4$ from the Mellin integrals in RadiationEntropyRelation.
In the broader Recognition chain this is pure equilibrium thermodynamics feeding cosmology, not a forcing-step (T0–T8) claim; it supplies the adiabatic-expansion input used when entropy and scale-factor evolution are later tied to recognition units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.