phaseSpacePressure_closed_form
plain-language theorem explainer
The three-dimensional grand-canonical phase-space pressure for massless Bose and Fermi sectors equals the Stefan–Boltzmann law $(\pi^2/90)(g_B+(7/8)g_F)T^4$. Cosmologists and RS auditors cite it as the end-to-end derivation of radiation pressure from the momentum integral, not a model ansatz. The proof is a two-step rewrite: identify the phase-space sum with the reduced plasma pressure, then apply that pressure's Mellin-closed form.
Claim. For real degeneracies $g_B$, $g_F$ and temperature $T>0$, the sum of the three-dimensional phase-space densities with the Bose log-kernel $-\ln(1-e^{-t})$ and the Fermi log-kernel $\ln(1+e^{-t})$ equals $\frac{\pi^2}{90}\bigl(g_B+\frac{7}{8}g_F\bigr)T^4$.
background
This module starts from the genuine 3D momentum integral
$P=(g/(2\pi)^3)\int d^3k,T,K(|k|/T)$
and derives the reduced one-dimensional form that GrandPotential had taken as definitional. The angular factor $1/(2\pi^2)$ and the $T^4$ scaling come from the co-area formula on Haar measure, the unit-ball volume in $\mathbb{R}^3$, and the substitution $k=T t$. The Stefan–Boltzmann exponent 4 is $D+1$ with $D=3$, and $D=3$ is forced upstream by T8.
phaseSpaceDensity d g T K is the grand-canonical integral of one massless sector in $d$ spatial dimensions with degeneracy $g$ and dimensionless kernel $K$. Pressure uses the log kernels: Bose $-\ln(1-e^{-t})$ and Fermi $\ln(1+e^{-t})$. Upstream, plasmaPressure_from_phaseSpace proves that the $d=3$ sum of those densities equals the reduced GrandPotential.plasmaPressure. Separately, plasmaPressure_eq collapses the remaining radial integrals via Mellin values $\pi^4/45$ and $7\pi^4/360$ to the closed Stefan–Boltzmann expression.
proof idea
One short rewrite chain. First apply plasmaPressure_from_phaseSpace (with the positivity hypothesis on $T$) to replace the sum of three-dimensional phase-space densities by GrandPotential.plasmaPressure gB gF T. Then apply GrandPotential.plasmaPressure_eq, which unfolds the reduced pressure and inserts the Bose and Fermi log-integral values, yielding $(\pi^2/90)(g_B+(7/8)g_F)T^4$. No new integral estimates are performed here.
why it matters
Closes the provenance ledger for radiation pressure in the cosmology stack: the prefactor $g/(2\pi^2)$ and the $T^4$ law are no longer MODEL inputs but theorems from the 3D integral plus Mellin evaluation. The fermionic weight $7/8$ appears independently in the pressure channel, matching the same factor in energy and entropy. The exponent 4 is identified with $D+1$ under the T8 forcing that spatial dimension is three, so Stefan–Boltzmann sits on the UnifiedForcingChain rather than on an external continuum assumption. No downstream users are recorded yet; the natural consumers are any later radiation-era or entropy-budget theorems that need the closed pressure without reopening the momentum integral.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.