potential_gibbs_duhem
plain-language theorem explainer
Along a temperature trajectory T(t), pressure satisfies d/dt P(T(t)) = s(T(t))·T'(t) whenever s = dP/dT. This is the Gibbs–Duhem identity used in FRW entropy bookkeeping, derived rather than postulated. Anyone citing grand-potential equilibrium in RS cosmology needs it. The proof is a one-line chain-rule composition of derivatives.
Claim. Let $P,s,T:\mathbb{R}\to\mathbb{R}$. If $P$ is differentiable at $T(t)$ with derivative $s(T(t))$, and $T$ is differentiable at $t$ with derivative $T'$, then $u\mapsto P(T(u))$ is differentiable at $t$ with derivative $s(T(t))\cdot T'$.
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$.
The module discharges the two equilibrium identities that EntropyConservationFRW previously took as named hypotheses: Euler ($T\cdot s=\rho+P$) and Gibbs–Duhem ($p'=s\cdot T'$ along a path). Gibbs–Duhem here is not an independent law; it is the chain rule on the definition $s=dP/dT$.
Local setting: FRW continuity plus these identities yields comoving entropy conservation. The concrete massless Bose/Fermi plasma later realizes $P\propto T^4$ via Mellin integrals from RadiationEntropyRelation.
proof idea
One-line term proof. Apply Mathlib's derivative composition (HasDerivAt.comp) to the outer map $P$ at the point $T(t)$ and the inner map $T$ at $t$, then rewrite the composite as Function.comp. No thermodynamic content enters beyond the two HasDerivAt hypotheses.
why it matters
This is the second structural discharge (with potential_euler) that collapses the two free hypotheses of comoving_entropy_conserved into one statement: pressure is a differentiable potential with $s=dP/dT$, i.e. local equilibrium at $\mu=0$.
Downstream, potential_energy_deriv builds the trajectory form $d/dt,\rho(T(t))=T\cdot s'(T)\cdot T'$ on top of it, and potential_entropy_conserved packages both identities to prove $d/dt(s\cdot a^3)=0$ from FRW continuity alone. That theorem's doc states the Euler and Gibbs–Duhem hypotheses are derived here, not assumed.
In the RS cosmology stack this closes the equilibrium interface between statistical mechanics of the plasma and FRW entropy conservation, without extra dynamical postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.