plasmaPressure
plain-language theorem explainer
Defines the pressure of a massless Bose/Fermi plasma as the sum of two grand-canonical log-kernel integrals, each scaled by g/(2π²)·T⁴. Cosmology proofs that need a concrete thermodynamic potential for the radiation sector cite this. The body is a direct transcription of the angular-reduced partition-function integrands after t = E/T.
Claim. For bosonic weight $g_B$, fermionic weight $g_F$, and temperature $T$, the plasma pressure is $P(g_B,g_F,T)=\frac{g_B}{2\pi^2}T^4\int_0^\infty t^2(-\ln(1-e^{-t}))\,dt+\frac{g_F}{2\pi^2}T^4\int_0^\infty t^2\ln(1+e^{-t})\,dt$.
background
In the grand-canonical ensemble at zero chemical potential the fluid is fixed by a single potential: the pressure $P(T)$ (equivalently grand-potential density $\Omega=-P$). Entropy density is $s=dP/dT$ and energy density is the Legendre transform $\rho=Ts-P$. The module uses that structure to discharge Euler ($Ts=\rho+P$) and Gibbs–Duhem ($P'=s,T'$) as pure consequences of differentiability, collapsing the two named hypotheses of comoving entropy conservation into one equilibrium statement.
Section 2 instantiates the potential with statistical mechanics. After angular integration and the substitution $t=E/T$, the Bose and Fermi sectors contribute the log kernels $-\ln(1-e^{-t})$ and $\ln(1+e^{-t})$ respectively, each with prefactor $g/(2\pi^2),T^4$. The companion energy density uses the occupation integrals $\int t^3/(e^t\mp 1),dt$ derived in the fermion-weight module. The closed values of the log integrals ($\pi^4/45$, $7\pi^4/360$) live upstream in the radiation-entropy relation via Mellin transforms.
proof idea
Pure definition: no proof obligations. The right-hand side is the sum of the bosonic and fermionic grand-canonical pressure integrands written as improper integrals over $(0,\infty)$, with the standard mode-density prefactor $g/(2\pi^2)$ and the $T^4$ scaling from the massless dispersion. Downstream theorems unfold this definition and rewrite the two integrals by their closed Mellin values.
why it matters
This is the concrete statistical-mechanical potential that turns the abstract Euler/Gibbs–Duhem discharge into a theorem about real radiation. Downstream, the closed-form identity collapses both log integrals to $P=(\pi^2/90)(g_B+(7/8)g_F)T^4$, recovering the familiar $7/8$ fermionic weight from the pressure channel alone. Differentiating that form shows $s=dP/dT$ equals the independently built radiation entropy, so the plasma is a potential fluid by theorem, not by fiat. Legendre consistency then matches $Ts-P$ against the occupation-number energy integral, and the equation of state $p=\rho/3$ drops out by algebra. Phase-space reduction later derives the $g/(2\pi^2),T^4$ prefactor from the $D=3$ momentum integral (angular factor $4\pi/(2\pi)^3$ and $T^{D+1}$ rescaling), so the definition is no longer free: it is the reduced 3D grand-canonical pressure. Together these steps close the equilibrium hypotheses that feed FRW entropy conservation and neutrino dilution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.