plasmaEnergy
plain-language theorem explainer
Defines the energy density of a massless Bose–Fermi plasma at temperature T as the sum of the two occupation integrals ∫ t³/(e^t∓1) dt, each scaled by g/(2π²) T⁴. Cosmologists cite it as the integral form of ρ before the closed-form reduction. The body is a pure definition: two improper integrals over (0,∞), no proof obligations.
Claim. For bosonic and fermionic effective degrees of freedom $g_B,g_F$ and temperature $T$, the plasma energy density is $$\rho(g_B,g_F,T)=\frac{g_B}{2\pi^2}T^4\int_0^\infty\frac{t^3}{e^t-1}\,dt+\frac{g_F}{2\pi^2}T^4\int_0^\infty\frac{t^3}{e^t+1}\,dt.$$
background
The GrandPotential module builds local equilibrium from a single thermodynamic potential: pressure $P(T)$ (grand potential density $\Omega=-P$) at vanishing chemical potential. Entropy density is $s=dP/dT$ and energy density is the Legendre transform $\rho=T s-P$. Euler $T s=\rho+P$ and Gibbs–Duhem then become structural identities, discharging the two named hypotheses that EntropyConservationFRW needed for comoving entropy conservation.
Section 2 realises that potential with statistical mechanics. Pressure uses the log-kernel integrals of the grand partition function; energy uses the occupation-number kernels $\int t^3/(e^t\mp 1),dt$. Those Bose and Fermi integrals are evaluated in FermionWeightIntegral (values $\pi^4/15$ and $7\pi^4/120$), the same $7/8$ fermionic weight that appears in entropy and pressure.
The prefactor $g/(2\pi^2)T^4$ is the standard massless 3D phase-space reduction; PhaseSpaceReduction later derives it from the full momentum integral rather than positing it.
proof idea
No proof: this is a noncomputable definition. The right-hand side is the sum of two scaled improper integrals over the positive reals, Bose kernel $t^3/(e^t-1)$ and Fermi kernel $t^3/(e^t+1)$. Downstream theorems unfold it and rewrite with FermionWeightIntegral.bose_integral_value and fermi_integral_value to reach the closed form.
why it matters
This is the integral anchor for the plasma energy channel in the grand-canonical story. plasmaEnergy_eq collapses it to $\rho=(\pi^2/30)(g_B+(7/8)g_F)T^4$. plasma_energyOf proves Legendre consistency: the abstract energy $T s-P$ built from plasma pressure and radiation entropy equals this integral form, so two independent ensemble routes agree. plasma_eos then forces the radiation equation of state $p=\rho/3$ from the closed forms alone, with no EOS input.
PhaseSpaceReduction.plasmaEnergy_from_phaseSpace and StatisticsKernels.plasmaEnergy_from_occupation identify the same object with the 3D phase-space integral of $E\cdot n(E/T)$ and with mean occupation times mode energy. Together they close the loop from partition functions through kernels to thermodynamic densities that feed FRW entropy conservation.
In the broader RS chain this is ordinary relativistic statistical mechanics instantiated inside the forced $D=3$ setting (T8), not a new forcing step; its role is to make the equilibrium identities used by cosmology fully discharged rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.