plasma_energyOf
plain-language theorem explainer
The Legendre energy T·s − P formed from the massless Bose/Fermi plasma pressure and radiation entropy equals the independently computed occupation-number energy density. Cosmologists verifying grand-canonical consistency of the radiation sector would cite this. After pointwise extension, the proof substitutes the three closed forms (pressure, entropy, energy) and finishes by ring algebra.
Claim. For any $g_B, g_F \in \mathbb{R}$, the Legendre energy density $\rho(T) = T\,s(T) - P(T)$ built from the plasma pressure $P$ and the radiation entropy density $s$ equals the plasma energy density obtained from the occupation-number integrals $\int_0^\infty t^3/(e^t\mp 1)\,dt$.
background
In the grand-canonical ensemble at zero chemical potential a fluid is fixed by one thermodynamic potential: the pressure $P(T)$ (equivalently $\Omega = -P$). Entropy density is $s = dP/dT$, and energy density is the Legendre transform $\rho = T,s - P$. The module shows that Euler ($T s = \rho + P$) and Gibbs–Duhem are then algebraic/chain-rule identities, so the two named hypotheses of comoving entropy conservation in FRW collapse to a single structural statement: local equilibrium.
Section 2 realises that structure for a massless Bose/Fermi plasma. Pressure comes from the log-kernel grand-partition integrals; its closed form is $P = (\pi^2/90)(g_B + (7/8)g_F)T^4$. Energy is defined independently via occupation-number integrals $\int t^3/(e^t\mp 1)$, closing to $\rho = (\pi^2/30)(g_B + (7/8)g_F)T^4$. Radiation entropy is the matching $s \propto T^3$ factor from the neutrino-dilution module.
The abstract operator energyOf is exactly $\rho(T) = T,s(T) - P(T)$. The claim is that feeding it the plasma pressure and radiation entropy recovers the occupation-number energy.
proof idea
Pointwise on temperature via functional extensionality. Unfold the Legendre definition $\rho = T s - P$. Rewrite with the three closed-form theorems: radiation entropy, plasma energy ($\pi^4/15$ and $7\pi^4/120$ channels), and plasma pressure ($\pi^4/45$ and $7\pi^4/360$ log-kernel channels). The resulting rational identity in $\pi$, $g_B$, $g_F$, and $T$ is discharged by ring.
why it matters
Doc-comment labels this Legendre consistency: two separate ensemble computations meet. The pressure channel (log kernels from the grand partition function) plus entropy, after the Legendre transform, agrees with the energy channel (occupation numbers). That is internal consistency of the grand-canonical structure, not an extra dynamical assumption.
The parent module uses this structure to discharge Euler and Gibbs–Duhem, which EntropyConservationFRW took as named hypotheses for comoving entropy conservation. With pressure a differentiable potential and $s = dP/dT$, those identities become definitions of local equilibrium. The radiation equation of state $p = \rho/3$ is then forced by the integrals rather than inserted by hand (sibling theorem immediately below).
No downstream consumers are wired yet (used_by empty); the natural landing sites are entropy-conservation and radiation-EOS lemmas in the cosmology chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.