potential_euler
plain-language theorem explainer
The Euler relation T·s = ρ + P holds identically once energy density is the Legendre transform ρ = T·s − P of a pressure potential. Cosmologists discharging equilibrium hypotheses in FRW entropy conservation cite it. The proof unfolds that definition and closes by ring cancellation; no dynamics or differentiability is used.
Claim. For real-valued functions $P$ and $s$ and any real $x$, $x\,s(x)=\rho(x)+P(x)$, where the energy density is the Legendre transform $\rho(x):=x\,s(x)-P(x)$.
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$. That is the per-volume form of $U=TS-PV+\mu N$ at $\mu=0$.
The parent module exists to discharge two equilibrium identities that EntropyConservationFRW previously took as named hypotheses: Euler ($T\cdot s=\rho+p$) and Gibbs–Duhem ($p'=s\cdot T'$). With the Legendre structure in place, Euler is pure algebra of the transform, not an independent postulate.
Upstream, the energy-density map packages exactly $\rho(T)=T\cdot s(T)-P(T)$. The present identity is the immediate rearrangement of that definition.
proof idea
Unfold the energy-density definition $\rho(x)=x,s(x)-P(x)$. The goal becomes the tautology $x,s(x)=(x,s(x)-P(x))+P(x)$, which the ring tactic closes. No lemmas beyond definitional simplification are required; the result is pointwise algebraic and holds for arbitrary real functions $P,s$.
why it matters
This is the first structural identity that lets the module collapse the two free hypotheses of comoving entropy conservation into one statement: pressure is a differentiable potential with $s=dP/dT$ (local equilibrium at $\mu=0$). Downstream, the entropy-conservation theorem applies Euler together with the chain-rule Gibbs–Duhem identity to prove that the FRW continuity equation forces $d/dt(s\cdot a^3)=0$ without extra dynamical assumptions. The energy-along-trajectory derivative theorem also depends on the same Legendre package. In the Recognition cosmology stack this removes independent postulates from the entropy argument used for radiation and plasma epochs, before the concrete Bose/Fermi pressure $P\propto T^4$ is instantiated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.