plasmaPressure_eq
plain-language theorem explainer
Closed-form Stefan–Boltzmann pressure for a massless Bose/Fermi plasma: P = (π²/90)(g_B + (7/8)g_F) T⁴. Cosmologists deriving the radiation EOS, entropy conservation, or g_* counting from the grand potential cite this. Proof unfolds the log-kernel integral definition, substitutes the two Mellin evaluations (π⁴/45, 7π⁴/360), and finishes by field simplification and ring.
Claim. For all real $g_B$, $g_F$, and $T$, the pressure of a massless Bose/Fermi plasma equals $\frac{\pi^2}{90}\bigl(g_B + \frac{7}{8} g_F\bigr) T^4$.
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=T s-P$. This module uses that structure to discharge the Euler and Gibbs–Duhem identities that EntropyConservationFRW previously took as named hypotheses.
The concrete plasma pressure is the log-kernel integral of the grand partition function after angular integration and $t=E/T$: $P=(g_B/2\pi^2)T^4\int_0^\infty t^2(-\ln(1-e^{-t})),dt+(g_F/2\pi^2)T^4\int_0^\infty t^2\ln(1+e^{-t}),dt$.
Those two improper integrals were evaluated in RadiationEntropyRelation via Mellin transforms: Bose kernel $\pi^4/45$, Fermi kernel $7\pi^4/360$.
proof idea
Unfold the definition of plasma pressure into the weighted sum of the two log-kernel integrals. Rewrite each integral by the closed values boseLog_integral_value ($\pi^4/45$) and fermiLog_integral_value ($7\pi^4/360$). After recording $\pi\neq 0$, field_simp clears the common $2\pi^2$ denominators and ring collapses the rational coefficients to the single prefactor $\pi^2/90$ with fermionic weight $7/8$.
why it matters
This is the concrete closed form that turns the abstract grand-potential structure into radiation thermodynamics. Downstream, plasmaPressure_potential shows $s=dP/dT$ matches the independently derived radiation entropy, so the plasma is a potential fluid by theorem rather than definition. plasma_energyOf checks Legendre consistency against the energy integrals, and plasma_eos forces $p=\rho/3$ with no EOS input. Outside the module, phaseSpacePressure_closed_form chains the same identity to the 3D momentum-space reduction, giving Stefan–Boltzmann end-to-end from phase space. Together these discharge the equilibrium hypotheses of comoving entropy conservation in FRW and close the radiation sector of the cosmology stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.