phaseSpaceEnergy_closed_form
plain-language theorem explainer
The Bose plus Fermi phase-space energy densities in three spatial dimensions equal the standard radiation formula (π²/30)(g_B + (7/8)g_F) T⁴. Cosmologists matching the 3D momentum integral to the reduced grand-potential energy cite this identity. The proof is a two-step rewrite: the phase-space form equals the 1D plasma energy, which already has the closed form.
Claim. For real degeneracies $g_B,g_F$ and temperature $T>0$, the sum of the three-dimensional phase-space energy densities with Bose kernel $t/(e^t-1)$ and Fermi kernel $t/(e^t+1)$ equals $\frac{\pi^2}{30}\,(g_B+\tfrac{7}{8}g_F)\,T^4$.
background
This module derives the familiar $g/(2\pi^2),T^4$ prefactor in the plasma pressure and energy from the underlying three-dimensional momentum integral $P=(g/(2\pi)^3)\int d^3k,T,K(|k|/T)$. The angular factor and $T^4$ scaling are not model inputs: they follow from radial co-area reduction of a Haar integral, the unit-ball volume in $\mathbb{R}^3$, and the substitution $k=T\cdot t$. Spatial dimension $D=3$ is the forced value from the upstream forcing chain (T8), so the Stefan–Boltzmann exponent 4 is $D+1$.
The energy kernels are the occupation-weighted factors: Bose $t/(e^t-1)$ and Fermi $t/(e^t+1)$. The phase-space density packages the full $d$-dimensional integral of a radial kernel at temperature $T$ with degeneracy $g$. Upstream, plasmaEnergy_from_phaseSpace identifies the $D=3$ Bose+Fermi phase-space sum with the one-dimensional reduced plasma energy, and GrandPotential.plasmaEnergy_eq already evaluates that reduced form to $(\pi^2/30)(g_B+(7/8)g_F)T^4$ via the classical Bose/Fermi weight integrals $\pi^4/15$ and $7\pi^4/120$.
proof idea
Two-line rewrite proof. First apply the in-module identification that the $D=3$ phase-space energy density (Bose plus Fermi kernels) equals the reduced plasma energy at the same $(g_B,g_F,T)$. Then rewrite by the GrandPotential closed form, which expands the reduced energy, inserts the Bose and Fermi integral values, and simplifies the $\pi$ prefactors to $\pi^2/30$. No new integral evaluation occurs here; the work is composition of those two equalities under $T>0$.
why it matters
Closes the energy side of the phase-space reduction ledger: the 3D momentum-space definition of radiation energy is identical to the textbook blackbody formula used in early-universe thermodynamics. Together with the sibling pressure closed form, it shows that both thermodynamic densities inherit the $1/(2\pi^2)$ angular factor and $T^4$ scaling from $D=3$ geometry rather than from an ad hoc 1D model. The exponent link is structural ($D+1$ with $D=3$ forced by T8), so the Stefan–Boltzmann law sits on the same forcing chain as the spatial dimension theorem. No downstream dependents are recorded yet; the natural consumers are cosmology lemmas that quote $\rho\propto T^4$ while remaining anchored to the Haar phase-space integral.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.