phaseSpaceDensity_T_scaling
plain-language theorem explainer
In any nonzero spatial dimension d, the grand-canonical phase-space density of a massless sector scales exactly as T^{d+1} relative to its unit-temperature value. Cosmologists and thermodynamicists cite this to derive the Stefan–Boltzmann T^4 law as pure dimensional analysis once D=3 is forced. The proof is a Haar co-area reduction plus the radial substitution y=T·t; the unit-ball volume never appears.
Claim. For every spatial dimension $d \neq 0$, degeneracy $g \in \mathbb{R}$, temperature $T > 0$, and kernel $K : \mathbb{R} \to \mathbb{R}$, the phase-space density satisfies $$P_d(g,T,K) = T^{d+1}\, P_d(g,1,K),$$ where $P_d$ is the integral $g/(2\pi)^d \int T\,K(\|k\|/T)\,d^dk$ over Euclidean momentum space $\mathbb{R}^d$.
background
The module PhaseSpaceReduction rebuilds the plasma pressure and energy densities from the underlying $d$-dimensional momentum integral, rather than assuming the reduced 1D form with a $T^4$ prefactor. The central object is the phase-space density: degeneracy $g$ times mode density $1/(2\pi)^d$ times $\int T,K(|k|/T),d^dk$ over EuclideanSpace $\mathbb{R}^d$. Pressure uses the Bose/Fermi log kernels; energy density uses $t/(e^t\mp 1)$.
The local goal is to show that both the angular factor $1/(2\pi^2)$ and the $T^4$ scaling are theorems once $D=3$ is forced upstream (T8 of the UnifiedForcingChain). The present result isolates the temperature scaling in arbitrary $d\neq 0$: one power of $T$ per momentum coordinate plus one from the kernel prefactor.
The key upstream lemma is radial_scale_pow: the substitution $y=T\cdot t$ pulls $T^{n+1}$ out of any radial integral weighted by $y^n$ with kernel argument $y/T$, unconditionally (Mathlib change-of-variables in junk-value semantics).
proof idea
Instantiate Nonempty (Fin d) from $d\neq 0$. Unfold the phase-space density definition, then apply MeasureTheory.integral_fun_norm_addHaar twice: once at temperature $T$ and once at unit temperature. After simplifying finrank and the unit-temperature case, rewrite the $T$-integrand to factor the constant $T$ out of the radial weight. Apply integral_const_mul and radial_scale_pow at exponent $n=d-1$ (valid since $d\ge 1$). The identity $(d-1)+1=d$ together with the outer $T$ yields $T^{d+1}$; a final ring closes the equality. The unit-ball volume cancels between the two sides and is never evaluated.
why it matters
This is the structural half of the Stefan–Boltzmann derivation inside Recognition Science. Downstream, stefan_boltzmann_from_D3 simply specialises to $d=3$ and obtains $P\propto T^4$. The module doc is explicit: the exponent 4 is not an independent thermodynamic input; it is $D+1$ with $D=3$, and $D=3$ is the T8 forcing theorem of UnifiedForcingChain.
In the broader framework the result converts a geometric theorem (spatial dimension forced to three) into the radiation law that feeds plasma pressure, energy density, and the grand-potential thermodynamics used in cosmology. It also justifies rewriting the MODEL-level definitions of plasmaPressure and plasmaEnergy as derived consequences of the 3D momentum integral, closing the provenance ledger for the $g/(2\pi^2)\cdot T^4$ prefactor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.