phaseSpacePressure_potential
plain-language theorem explainer
At positive temperature, the T-derivative of the 3D Bose+Fermi phase-space pressure equals the radiation entropy density built from the independent entropy integrals. Cosmologists and statistical-mechanics auditors cite it to anchor s=dP/dT at the grand-canonical momentum integral rather than at a reduced 1D model. The proof transfers the existing reduced-form potential theorem by eventual equality on T>0 via the phase-space reduction identity.
Claim. Fix bosonic and fermionic degeneracies $g_B,g_F\in\mathbb{R}$ and a temperature $x>0$. Let $P_{\mathrm{ph}}(T)$ be the sum of the three-dimensional grand-canonical phase-space integrals with mode density $1/(2\pi)^3$, dispersion $E=\|k\|$, and the Bose/Fermi pressure kernels $-\ln(1-e^{-t})$ and $\ln(1+e^{-t})$. Then $P_{\mathrm{ph}}$ is differentiable at $x$ with derivative equal to the radiation entropy density $s(g_B,g_F,x)$.
background
This module starts from the three-dimensional grand-canonical pressure
$P=(g/(2\pi)^3)\int d^3k,T,K(|k|/T)$
and derives the familiar reduced form $P=(g/2\pi^2),T^4\int t^2 K(t),dt$. The angular factor $1/(2\pi^2)$ and the $T^4$ scaling are theorems here, not model inputs; the Stefan–Boltzmann exponent 4 is $D+1$ with $D=3$ forced upstream.
phaseSpaceDensity packages one massless sector in $d$ dimensions. The Bose and Fermi pressure kernels are $-\ln(1-e^{-t})$ and $\ln(1+e^{-t})$. The sibling theorem plasmaPressure_from_phaseSpace identifies the $d=3$ sum of those integrals with the earlier one-dimensional plasmaPressure.
Upstream, plasmaPressure_potential already proves that the temperature derivative of the reduced pressure is exactly radiationEntropy (the object built from the independent entropy-functional integrals $\int\sigma_B$, $\int\sigma_F$). The present result lifts that identity to the unreduced 3D integral.
proof idea
Start from the upstream theorem that the reduced plasma pressure has derivative equal to radiation entropy at the given positive temperature. Apply HasDerivAt.congr_of_eventuallyEq: on a neighborhood of that temperature (the open ray $T>0$), the phase-space sum equals the reduced pressure by plasmaPressure_from_phaseSpace. The two maps therefore share the same derivative at the point. No fresh differentiation or integrability argument is needed.
why it matters
Doc-comment calls this the capstone of the chain
3D phase space → 1D reduction → potential $P(T)$ → $s=P'$ → Euler $\rho=Ts-P$ → $g_{*s}$, dilution $4/11$, $p=\rho/3$.
The thermodynamic relation $s=dP/dT$ is no longer tied to a definitional 1D model; it sits on the grand-canonical momentum integral, with only mode density $1/(2\pi)^3$, $E=|k|$, and the statistics kernels as upstream inputs. The $T^4$ scaling itself is $D+1$ with $D=3$ from the T8 dimension forcing in the unified chain. No downstream consumers are wired yet; the declaration closes the provenance ledger for the pressure side of the relativistic plasma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.