energy_deriv
plain-language theorem explainer
Differentiating the Legendre energy density ρ = T·s − P of a grand-potential fluid yields ρ′(T) = T·s′(T). Cosmologists citing the fundamental relation dρ = T ds in the zero-chemical-potential ensemble use this. The proof is a short calculus argument: product rule on T·s, subtract P′, then cancel the bare s terms by ring.
Claim. Let $P,s:\mathbb{R}\to\mathbb{R}$ and fix $x,s_T\in\mathbb{R}$. If $P'(x)=s(x)$ and $s'(x)=s_T$, then the energy density $\rho(x)=x\,s(x)-P(x)$ is differentiable at $x$ with $\rho'(x)=x\,s_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$. That is exactly energyOf: $\rho(x)=x,s(x)-P(x)$.
The module discharges the two equilibrium identities that EntropyConservationFRW took as named hypotheses. Euler $T,s=\rho+P$ is algebraic in the Legendre transform; Gibbs–Duhem is the chain rule on $P(T(t))$. The present result is the remaining fundamental relation: differentiating $\rho=T,s-P$ produces $s+T,s'-s$, hence $\rho'=T,s'$.
Energy here is the plain real type used throughout RS-native units; no extra structure is required beyond differentiability of $P$ and $s$ at the evaluation point.
proof idea
Start from the identity derivative $\mathrm{id}'=1$. Multiply by $s$ via the product rule to get $(x\mapsto x,s(x))'=s(x)+x,s_T$. Subtract the given derivative of $P$ to obtain
$$(x\mapsto x,s(x)-P(x))'=s(x)+x,s_T-s(x).$$
A one-line ring rewrite cancels the bare $s(x)$ terms, leaving $x,s_T$. The resulting HasDerivAt statement is exactly the claim for energyOf P s.
why it matters
This is the static (temperature-only) form of $d\rho=T,ds$ that the module advertises as collapsing two FRW hypotheses into one structural fact: pressure is a differentiable potential with $s=dP/dT$. Downstream, potential_energy_deriv composes with a temperature trajectory $T(t)$ by the chain rule, giving $d/dt,\rho(T(t))=T,s'(T),T'$. That trajectory form, together with Euler and Gibbs–Duhem, feeds potential_entropy_conserved and thereby discharges the equilibrium side of comoving entropy conservation in FRW.
In the Recognition cosmology stack this is pure thermodynamics, not a new dynamical postulate: once the plasma pressure is realized as the Bose/Fermi log-kernel integral ($P\propto T^4$), the same derivative identities apply automatically. No forcing-chain landmark (T5–T8) is invoked here; the result is local equilibrium structure used by the radiation and entropy modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.