potential_entropy_deriv
plain-language theorem explainer
Along a temperature trajectory T(t), the composite entropy density s(T(t)) has time derivative s'(T)·T'. Cosmology proofs that track comoving entropy under FRW evolution cite this as the chain-rule step for s∘T. The proof is a one-line application of HasDerivAt composition, rewritten via Function.comp.
Claim. If $s:\mathbb{R}\to\mathbb{R}$ is differentiable at $T(t)$ with derivative $s_T$, and $T:\mathbb{R}\to\mathbb{R}$ is differentiable at $t$ with derivative $T'$, then the composite $u\mapsto s(T(u))$ is differentiable at $t$ with derivative $s_T\cdot T'$.
background
In the grand-canonical ensemble at zero chemical potential, a fluid is fixed by a single 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 hypotheses: Euler $T\cdot s=\rho+P$ (algebraic from the Legendre transform) and Gibbs–Duhem $dP/dt=s\cdot T'$ (chain rule on $P\circ T$). The fundamental relation $d\rho=T,ds$ follows by differentiating $\rho=T\cdot s-P$.
This lemma is the pure chain-rule fragment for entropy along a temperature path: once $s$ is differentiable in $T$ and $T$ is differentiable in $t$, the composite $s(T(t))$ has the expected product derivative. It is the entropy-side counterpart of the Gibbs–Duhem chain rule on $P$.
proof idea
One-line term proof. Apply the Mathlib chain rule HasDerivAt.comp to the pair of derivative hypotheses hs (for $s$ at $T(t)$) and hT (for $T$ at $t$), then simpa with Function.comp to match the composite fun u => s (T u). No thermodynamic content enters; the argument is pure real analysis.
why it matters
Parent theorem potential_entropy_conserved uses this (with Euler and Gibbs–Duhem from the same module) to prove that FRW continuity alone forces $d/dt(s\cdot a^3)=0$ whenever pressure is a differentiable potential with $s=dP/dT$. That collapses the two named hypotheses of comoving_entropy_conserved into one structural statement: local equilibrium at zero chemical potential.
In the Recognition cosmology stack this is the analytic glue between the grand-potential definitions and comoving entropy conservation, before the concrete massless Bose/Fermi plasma ($P\propto T^4$ from the Mellin integrals in RadiationEntropyRelation) is plugged in. It does not itself invoke the forcing chain (T0–T8) or the $\phi$-ladder; it is classical thermo-calculus supporting the RS FRW entropy story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.