phaseSpaceDensity
plain-language theorem explainer
Grand-canonical phase-space density for one massless sector in d spatial dimensions: degeneracy g, mode density (2π)^{-d}, and the integral of T·K(‖k‖/T) over Euclidean momentum space. Cosmology and radiation-thermodynamics proofs cite it as the unreduced d-dimensional starting point before radial reduction to the familiar 1D Mellin form. The body is a direct integral definition (no derived equality).
Claim. For $d\in\mathbb{N}$, degeneracy $g\in\mathbb{R}$, temperature $T\in\mathbb{R}$, and dimensionless kernel $K:\mathbb{R}\to\mathbb{R}$, the phase-space density is $\dfrac{g}{(2\pi)^d}\displaystyle\int_{\mathbb{R}^d} T\,K\bigl(\lVert k\rVert/T\bigr)\,d^dk$, with $E=\lVert k\rVert$ on Euclidean space of dimension $d$.
background
The module Phase-Space Reduction starts from the unreduced grand-canonical momentum integral and derives the reduced 1D form that GrandPotential had taken as a modeling definition. In that reduced form, plasma pressure and energy appear as $(g/2\pi^2)\cdot T^4\int t^2 K(t),dt$; here the angular factor $4\pi/(2\pi)^3=1/(2\pi^2)$ and the $T^4$ scaling are no longer inputs.
The kernel $K$ is dimensionless and evaluated at $E/T$ with $E=\lVert k\rVert$. For pressure one takes the Bose log kernel $-\ln(1-e^{-t})$ or the Fermi log kernel $\ln(1+e^{-t})$ (from $\pm T\ln Z$ per mode). For energy density one takes $t/(e^t\mp 1)$, i.e. $E\cdot n(E/T)$ rescaled by $T$. Mode density is the standard $(2\pi)^{-d}$.
Local setting: both the radial co-area reduction of a Haar integral of a norm-dependent function and the substitution $k=T\cdot t$ are available unconditionally in Mathlib junk-value semantics. The Stefan–Boltzmann exponent 4 is identified as $D+1$ with $D=3$ forced upstream (T8).
proof idea
Pure definition: scale the integral of $T\cdot K(\lVert k\rVert/T)$ over EuclideanSpace $\mathbb{R}^{\mathrm{Fin},d}$ by the prefactor $g/(2\pi)^d$. No lemmas are applied; downstream theorems unfold this def and invoke radial reduction (integral_norm_fin_three / integral_fun_norm_addHaar) plus the change of variables $k=T\cdot t$.
why it matters
This is the unreduced anchor for the whole module. phaseSpaceDensity_reduction equates the $d=3$ instance to $(g/2\pi^2)\cdot T^4\int_{t>0} t^2 K(t),dt$, discharging the MODEL status of the GrandPotential 1D form. phaseSpaceDensity_T_scaling proves $P_d(T)=T^{d+1}P_d(1)$ for any $d\neq 0$, so the Stefan–Boltzmann power is structural ($D+1$), not an extra axiom; stefan_boltzmann_from_D3 specializes at $d=3$, tying the exponent to T8 ($D=3$).
Closed-form parents chain through it: phaseSpacePressure_closed_form and phaseSpaceEnergy_closed_form recover $(\pi^2/90)(g_B+(7/8)g_F)T^4$ and $(\pi^2/30)(g_B+(7/8)g_F)T^4$ end-to-end from the 3D integral. plasmaPressure_from_phaseSpace / plasmaEnergy_from_phaseSpace identify the Bose/Fermi specializations with GrandPotential. The capstone phaseSpacePressure_potential then differentiates the 3D pressure to radiation entropy, anchoring the Euler chain $\rho=Ts-P$, dilution $4/11$, and $p=\rho/3$ at the grand-canonical momentum integral.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.