plasmaPressure_from_partitionFunction
plain-language theorem explainer
Plasma pressure for a massless Bose–Fermi gas equals the 3D phase-space integral of T ln Z_mode, with each mode partition built only from Gibbs weights and occupancy sets. Cosmologists deriving radiation pressure from first principles on the η_B chain would cite this. The proof rewrites the log-partition integrands as the classical Bose/Fermi kernels, then applies the existing phase-space reduction to the grand-potential formula.
Claim. For degeneracies $g_B,g_F\in\mathbb{R}$ and temperature $T>0$, the sum of the three-dimensional phase-space densities of $\ln Z_B$ and $\ln Z_F$ equals the grand-canonical plasma pressure $P(g_B,g_F,T)$. Here $Z_B(t)=\sum_{n\in\mathbb{N}}e^{-nt}$ and $Z_F(t)=\sum_{n\in\{0,1\}}e^{-nt}$ with dimensionless $t=E/T$, and the phase-space density carries the mode measure $g/(2\pi)^3$ times $T$ times the kernel.
background
This module derives the standard Bose and Fermi statistical kernels from single-mode grand partition functions at vanishing chemical potential. The only inputs are the Gibbs weight $e^{-n t}$ and the occupancy sets: unrestricted $n\in\mathbb{N}$ for bosons, Pauli-restricted $n\in{0,1}$ for fermions.
The Bose partition is the geometric series $Z_B=(1-e^{-t})^{-1}$; the Fermi partition is the two-state sum $Z_F=1+e^{-t}$. Their logarithms recover the pressure kernels $-\ln(1-e^{-t})$ and $\ln(1+e^{-t})$ that PhaseSpaceReduction and GrandPotential previously took as definitions. Upstream, plasma pressure is the classical integral $(g/2\pi^2)T^4\int_{0}^{\infty}t^2(\mp\ln(1\mp e^{-t})),dt$ per sector, and the phase-space reduction theorem already shows that the 3D densities of those kernels equal that formula.
The present result pushes the starting point one step further back: from the kernels to $\ln Z$ itself, so pressure begins from $\sum e^{-nE/T}$ in momentum space.
proof idea
Two pointwise identities identify $\ln Z_B$ with the Bose log-kernel and $\ln Z_F$ with the Fermi log-kernel (for $t>0$ on the Bose side). Each identity is lifted through a positivity-preserving congruence of the phase-space density functional, so the left-hand side becomes the sum of the classical Bose and Fermi kernel densities. The existing theorem that those 3D densities equal the grand-potential plasma pressure finishes the argument in one rewrite.
why it matters
This is the pressure capstone of StatisticsKernels: plasma pressure on the η_B chain now starts from mode partition functions $\sum e^{-nE/T}$ rather than from hand-inserted log kernels. It closes the provenance gap between the grand-canonical identity $P=(T/V)\ln Z$ and the cosmological pressure formula that GrandPotential previously treated as definitional.
Together with the companion energy capstone (energy as the phase-space integral of $E\cdot\langle n\rangle$), it locks thermodynamic consistency: pressure and energy kernels are derivative-related through $\langle n\rangle=-\partial_t\ln Z$, as the grand-canonical formalism demands. No downstream consumers are wired yet; natural landing sites are any derivation that assumed the grand-potential pressure formula as a model input.
In the Recognition Science stack this lives in the cosmology layer rather than the T0–T8 forcing chain, but it hardens the statistical-mechanics substrate that radiation and early-universe calculations rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.