energyOf
plain-language theorem explainer
Defines the energy density of a thermodynamic fluid as the Legendre transform ρ(T) = T·s(T) − P(T) of a pressure potential, with entropy density s identified as dP/dT. Cosmologists working the RS grand-potential route to neutrino dilution and g*s cite it as the structural definition of ρ at μ = 0. The body is a one-line function abbreviation, not a proof.
Claim. Given real functions $P$ (pressure potential) and $s$ (entropy density), the energy density is the map $\rho(x) = x\, s(x) - P(x)$. When $s = dP/dT$, this is the standard Legendre transform $\rho = T(\partial P/\partial T) - P$, i.e. the grand-canonical relation $U = TS - PV$ per unit volume at vanishing chemical potential.
background
The module discharges the two equilibrium identities that EntropyConservationFRW previously took as hypotheses: the Euler relation $T\cdot s = \rho + P$ and Gibbs–Duhem $P' = s\cdot T'$. In the grand-canonical ensemble at $\mu = 0$, a fluid is fixed by a single potential — the pressure $P(T)$ (equivalently grand-potential density $\Omega = -P$). Entropy density is defined by $s = dP/dT$; energy density is then the Legendre transform of that potential.
This definition is exactly that transform: $\rho(T) = T\cdot s(T) - P(T)$. Once it is in place, Euler becomes an algebraic identity of the Legendre structure, Gibbs–Duhem is the chain rule along a temperature trajectory, and the fundamental relation $d\rho = T, ds$ follows by differentiation. The concrete massless Bose/Fermi plasma later instantiates $P$ via the log-kernel integrals already derived in RadiationEntropyRelation.
proof idea
Pure definition: the body is the lambda fun x => x * s x - P x. No tactics, no lemmas. Downstream theorems (potential_euler, energy_deriv, plasma_energyOf) unfold this abbreviation and apply product/chain rules or rewrite with the plasma closed forms.
why it matters
This is the structural hinge of the GrandPotential module. Every major theorem in the file consumes it: potential_euler (Euler as algebra), energy_deriv and potential_energy_deriv (fundamental relation $d\rho = T, ds$), potential_entropy_conserved / potential_entropy_constant (comoving entropy from the potential alone), and the plasma consistency check plasma_energyOf (Legendre energy matches the independent energy integral).
The two capstones dilution_from_potential and gStarS_from_potential then drop the Euler and Gibbs–Duhem hypotheses that EntropyConservationFRW required: only FRW continuity, a differentiable pressure potential with $s = dP/dT$, and boundary data remain. That collapses the thermodynamic input for the RS neutrino-dilution factor $(T_\nu/T_\gamma)^3 = 4/11$ and the present-day $g_{*s} = 43/11$ prefactor into a single local-equilibrium definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.