phaseSpaceDensity_reduction
plain-language theorem explainer
In three spatial dimensions the grand-canonical momentum integral of any radial kernel K collapses to a one-dimensional radial integral with prefactor g/(2π²)·T⁴. Cosmologists deriving plasma pressure and energy from first principles cite this identity. The proof unfolds the 3D density, applies the D=3 co-area reduction, swaps constants, and rescales the radial variable by T.
Claim. For degeneracy $g\in\mathbb{R}$, temperature $T>0$, and any kernel $K:\mathbb{R}\to\mathbb{R}$, $$\frac{g}{(2\pi)^3}\int_{\mathbb{R}^3} T\,K\!\left(\frac{\|k\|}{T}\right)\,d^3k = \frac{g}{2\pi^2}\,T^4\int_0^\infty t^2 K(t)\,dt.$$
background
The module PhaseSpaceReduction closes a modeling gap in GrandPotential: plasma pressure and energy were defined already in the reduced one-dimensional form $P=(g/2\pi^2),T^4\int t^2 K(t),dt$, with the angular factor and $T^4$ scaling built into the definition. Here those factors are derived from the underlying three-dimensional mode integral $(g/(2\pi)^3)\int d^3k,T,K(|k|/T)$.
The phase-space density is the Haar integral of a norm-dependent kernel over Euclidean momentum space $\mathbb{R}^3$, weighted by degeneracy $g$ and the usual $(2\pi)^{-3}$ mode density. The key upstream lemma is the radial reduction in $D=3$: any integral of $f(|k|)$ equals $4\pi\int_0^\infty y^2 f(y),dy$, with the $4\pi$ arising as $3\times\mathrm{vol}(B^3)=3\times(4\pi/3)$. A companion radial scaling lemma implements the substitution $k=T,t$ that produces the $T^4$ power.
Nothing about the kernel is used, so the same identity covers pressure (log kernels), energy, entropy, and number density. The Stefan–Boltzmann exponent 4 is $D+1$ with $D=3$, and $D=3$ is forced upstream by the T8 step of the unified forcing chain.
proof idea
Unfold the definition of the three-dimensional phase-space density. Apply the radial co-area theorem integral_norm_fin_three to the rescaled kernel $y\mapsto T,K(y/T)$, obtaining the factor $4\pi$ times a radial integral of $y^2,T,K(y/T)$. Factor $T$ out of the integrand by a pointwise ring identity and integral_const_mul. Invoke radial_scale_pow at power 2 to change variables $y=T,t$, which contributes $T^3$ from the measure and yields overall $T^4$. Finish with field_simp and ring, using $\pi\neq 0$, to rewrite $4\pi/(2\pi)^3$ as $1/(2\pi^2)$.
why it matters
This is the central reduction that turns a modeling assumption into a theorem. Downstream, plasmaPressure_from_phaseSpace and plasmaEnergy_from_phaseSpace rewrite the Bose/Fermi log and energy kernels through this identity and match them exactly to the previously definitional GrandPotential.plasmaPressure and plasmaEnergy. The doc-comment states the point: the $g/(2\pi^2)\cdot T^4$ prefactor is now derived.
In the Recognition framework the result ties cosmology to the forcing chain: the angular factor is pure $D=3$ geometry, and the temperature power is $D+1$, so Stefan–Boltzmann scaling is not an independent input once T8 has forced three spatial dimensions. The module ledger tags the $1/(2\pi^2)$ prefactor and the $T^4$ scaling as THEOREM rather than MODEL. Closed-form siblings (phaseSpacePressure_closed_form, phaseSpaceEnergy_closed_form) sit one layer above this reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.