plasmaEnergy_from_phaseSpace
plain-language theorem explainer
The three-dimensional momentum integral of E·n(E/T) for a massless Bose–Fermi plasma equals the reduced one-dimensional plasma energy density used downstream. Anyone deriving the Stefan–Boltzmann energy form from first principles cites this bridge. The proof applies the D=3 radial reduction to both sectors, then matches kernels by elementary algebra: t²·(t/(eᵗ∓1)) becomes t³/(eᵗ∓1).
Claim. For real degeneracies $g_B,g_F$ and temperature $T>0$, the sum of the $d=3$ phase-space densities with Bose energy kernel $t/(e^t-1)$ and Fermi energy kernel $t/(e^t+1)$ equals the plasma energy density $\frac{g_B}{2\pi^2}T^4\int_0^\infty t^3/(e^t-1)\,dt+\frac{g_F}{2\pi^2}T^4\int_0^\infty t^3/(e^t+1)\,dt$.
background
This module starts from the genuine three-dimensional grand-canonical integral
$P = g/(2\pi)^d \int d^d k, T, K(|k|/T)$
and derives the familiar reduced form with prefactor $g/(2\pi^2),T^4$. The angular factor $4\pi/(2\pi)^3 = 1/(2\pi^2)$ and the $T^4$ scaling are theorems here, not model inputs. Spatial dimension is fixed at $D=3$ by the upstream forcing chain (T8).
The phase-space density packages degeneracy $g$, temperature $T$, and a dimensionless kernel $K$ evaluated at $E/T$ with $E=|k|$. For energy density the kernels are the occupation-weighted factors $t/(e^t\mp 1)$ (Bose and Fermi). The target plasma energy is the already-reduced one-dimensional expression built from $\int t^3/(e^t\mp 1),dt$ with the same $g/(2\pi^2),T^4$ prefactor.
The key upstream lemma is the unconditional D=3 reduction: $(g/(2\pi)^3)\int d^3k, T,K(|k|/T) = (g/2\pi^2),T^4\int_0^\infty t^2 K(t),dt$, obtained from co-area/Haar radial collapse, unit-ball volume $4\pi/3$, and the substitution $k=T,t$.
proof idea
Rewrite both Bose and Fermi phase-space densities by the D=3 reduction lemma, producing prefactors $g/(2\pi^2),T^4$ times $\int t^2 K(t),dt$. Unfold the target plasma energy and the two energy kernels. The remaining gap is purely algebraic: pointwise $t^2\cdot(t/(e^t-1))=t^3/(e^t-1)$ and $t^2\cdot(t/(e^t+1))=t^3/(e^t+1)$, each discharged by funext and ring. After those rewrites the two sides match definitionally.
why it matters
This is the energy twin of the pressure reduction: it identifies the three-dimensional integral of $E\cdot n(E/T)$ with the grand-potential energy density, so later closed-form work can stay in the reduced layer. Downstream, the closed-form energy theorem rewrites through this identity and the known Mellin values to obtain $(\pi^2/30)(g_B+(7/8)g_F),T^4$. The statistics-kernels capstone likewise routes occupation-number integrals through the same equality.
Framework-wise the Stefan–Boltzmann exponent 4 is not free: it is $D+1$ with $D=3$ forced by T8 in the unified forcing chain. The module therefore converts a geometric fact (three spatial dimensions) into the thermodynamic $T^4$ law for massless plasma energy, end-to-end from Haar measure on momentum space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.