plasmaPressure_from_phaseSpace
plain-language theorem explainer
The three-dimensional grand-canonical pressure integral over Bose and Fermi log kernels equals the reduced one-dimensional plasma pressure with prefactor g/(2π²)·T⁴. Cosmologists deriving Stefan–Boltzmann radiation from first principles cite this bridge. The proof rewrites each sector by the radial phase-space reduction, unfolds the kernels and the target definition, and closes by reflexivity.
Claim. For real degeneracies $g_B,g_F$ and temperature $T>0$, the sum of the three-dimensional phase-space densities at spatial dimension $3$ with the Bose kernel $-\log(1-e^{-t})$ and the Fermi kernel $\log(1+e^{-t})$ equals the grand-potential plasma pressure $P(g_B,g_F,T)=(g_B/(2\pi^2))T^4\int_0^\infty t^2(-\log(1-e^{-t}))\,dt+(g_F/(2\pi^2))T^4\int_0^\infty t^2\log(1+e^{-t})\,dt$.
background
In the GrandPotential module, plasma pressure was introduced already in reduced one-dimensional form: each sector carries the prefactor $g/(2\pi^2)\cdot T^4$ times an integral of $t^2$ against a log kernel. That angular factor and the $T^4$ scaling were definitional inputs (MODEL), not derived.
This module starts from the underlying three-momentum integral $P=(g/(2\pi)^3)\int d^3k,T,K(|k|/T)$ and recovers the reduced form. The tools are the co-area (radial) reduction of a Haar integral of a norm-dependent function, the volume of the unit ball in $\mathbb{R}^3$, and the substitution $k=T\cdot t$. Both Bose and Fermi pressure kernels are the standard grand-canonical $\ln Z$ integrands after angular integration: $-\log(1-e^{-t})$ and $\log(1+e^{-t})$.
Spatial dimension enters as the constant $D=3$ forced upstream by the Recognition forcing chain (T8). The Stefan–Boltzmann exponent $4$ is then $D+1$, not an independent input.
proof idea
Apply the radial reduction lemma twice: once for the Bose sector with degeneracy $g_B$, once for the Fermi sector with $g_F$, each under $T>0$. That rewrites both three-dimensional phase-space densities into the one-dimensional $g/(2\pi^2)\cdot T^4$ shape with the corresponding kernel. Unfold the target plasma-pressure definition together with the two log-kernel abbreviations; the two sides match definitionally, so reflexivity finishes.
why it matters
This is the identification step that turns a MODEL prefactor into a THEOREM: the $1/(2\pi^2)$ angular factor and $T^4$ scaling now come from $D=3$ phase space rather than from the definition of plasma pressure. Downstream, the closed-form theorem chains this equality with the Mellin values of the log integrals to obtain $P=(\pi^2/90)(g_B+(7/8)g_F)T^4$, Stefan–Boltzmann with the fermionic $7/8$ end-to-end from the momentum integral. The potential theorem uses it to anchor $s=dP/dT$ at the same three-dimensional integral, feeding the Euler relation, neutrino dilution $4/11$, and $p=\rho/3$. A further capstone in StatisticsKernels rewrites the kernels as $\log Z$ of the Bose/Fermi partition functions, so only Gibbs weights and occupancy sets remain as inputs. Framework landmark: $D=3$ from T8 forces the exponent $4=D+1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.