plasmaEnergy_from_occupation
plain-language theorem explainer
Plasma energy density equals the 3D phase-space integral of mode energy times mean occupation, with Bose and Fermi occupations taken from the single-mode grand partition functions at μ=0. Cosmologists deriving ρ from Z_mode rather than from postulated kernels cite this. The proof rewrites the occupation integrands to the classical energy kernels, then applies the existing phase-space reduction.
Claim. For degeneracies $g_B,g_F\in\mathbb{R}$ and temperature $T>0$, the sum of the three-dimensional phase-space densities of $t\mapsto t\,\langle n\rangle_B(t)$ and $t\mapsto t\,\langle n\rangle_F(t)$ equals the plasma energy density $\rho(g_B,g_F,T)$ built from $\int_0^\infty t^3/(e^t\mp 1)\,dt$.
background
The StatisticsKernels module derives the Bose/Fermi pressure and energy kernels from the single-mode grand partition function at vanishing chemical potential. Occupancies run over $\mathbb{N}$ for bosons and ${0,1}$ for fermions; the Gibbs weight is $e^{-n t}$ with $t=E/T$. From $Z_B=(1-e^{-t})^{-1}$ and $Z_F=1+e^{-t}$ one obtains the mean occupations $\langle n\rangle_B=1/(e^t-1)$ and $\langle n\rangle_F=1/(e^t+1)$.
Earlier, PhaseSpaceReduction treated the energy kernels $t/(e^t\mp 1)$ as model inputs and proved that their 3D phase-space integrals recover GrandPotential.plasmaEnergy (the standard $\int t^3/(e^t\mp 1),dt$ form scaled by $g T^4/(2\pi^2)$). The present module's energy-kernel identities state that those kernels are exactly $t\cdot\langle n\rangle$.
phaseSpaceDensity packages the grand-canonical integral over momentum space in $d$ spatial dimensions with degeneracy $g$, temperature $T$, and a dimensionless kernel $K$.
proof idea
Two congruence steps, then the prior reduction. First, phaseSpaceDensity_congr_pos rewrites the Bose integrand $t\cdot\langle n\rangle_B(t)$ to boseEnergyKernel, using boseEnergyKernel_eq_occupation (pointwise for $t>0$). The same congruence with fermiEnergyKernel_eq_occupation handles the Fermi sector. After those rewrites, the goal is exactly plasmaEnergy_from_phaseSpace, which is applied directly.
why it matters
This is the energy capstone of StatisticsKernels: plasma energy no longer begins from postulated kernels $t/(e^t\mp 1)$, but from $\sum_n e^{-n E/T}$ in momentum space, via occupation numbers. It sits parallel to plasmaPressure_from_partitionFunction on the pressure side. Together they close the provenance ledger that PhaseSpaceReduction and GrandPotential took as MODEL definitions.
In the Recognition cosmology stack this feeds the $\eta_B$ and $g_$ energy-density chain: once occupations come from $Z_\mathrm{mode}$, the $T^4$ radiation energy and the eight-tick thermal bookkeeping inherit a partition-function origin rather than an ansatz. No downstream theorem currently cites it (used_by is empty), so it is a terminal identity ready for number-density and $g_$ consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.