Pith. sign in
module module high

IndisputableMonolith.Cosmology.PhaseSpaceReduction

show as:
view Lean formalization →

Grand-canonical phase-space integrals for one massless Bose or Fermi sector in d spatial dimensions, with degeneracy g and temperature T. Pressure and energy density appear as mode-density times a radial integral of a dimensionless kernel K(E/T) at E=‖k‖. Cosmologists in the RS thermal-history stack cite the d=3 reductions that feed plasma p and ρ. The module defines the kernels, the (2π)^{-d} density, and the radial lemmas that close those integrals.

claimIn $d$ spatial dimensions the grand-canonical phase-space integral of one massless sector with degeneracy $g$ and temperature $T$ is $\frac{g}{(2\pi)^d}\int K(\|k\|/T)\,d^d k$, where pressure uses $K(t)=-\ln(1-e^{-t})$ (Bose) or $K(t)=\ln(1+e^{-t})$ (Fermi), and energy density uses $K(t)=t/(e^t\mp 1)$. Closed forms specialize the radial reduction at $d=3$.

background

The module sits in the cosmology thermal-history stack directly above GrandPotential. That upstream module records Euler and Gibbs–Duhem identities ($T\cdot s=\rho+p$ and related equilibrium relations) used to obtain comoving entropy conservation from the FRW continuity equation. PhaseSpaceReduction supplies the explicit integral expressions for pressure and energy density of a massless ideal sector that make those identities concrete.

Objects introduced: phase-space density with mode factor $1/(2\pi)^d$; Bose and Fermi log-kernels for pressure, read off from $\pm T\ln Z$ per mode; energy kernels $t/(e^t\mp 1)$, i.e. $E\cdot n(E/T)$ rescaled by $T$. Supporting lemmas cover the integral of a radial function of $|k|$ in finite dimension and power scaling under $k\mapsto T u$, so the $d$-dimensional integral collapses to a one-dimensional radial form times $T^{d+1}$.

proof idea

Definition-and-reduction module, not a single deep theorem. Bose/Fermi pressure and energy kernels are introduced as MODEL definitions. The phase-space density packages degeneracy, mode factor, and the kernel evaluated at $|k|/T$. Radial lemmas (finite-dimensional norm integral, scaling $k=Tu$) convert the $d$-dimensional integral into a standard one-dimensional form. Pressure and energy of the plasma are then identified with those reduced integrals; at $d=3$ the closed-form statements follow by specialization. No derivation of the kernels from $\ln Z$ is attempted here.

why it matters in Recognition Science

Feeds the two modules that build the statistical-mechanics floor under the thermal-history chain. PartitionKernels imports it to attach per-mode grand partition functions and mean occupation numbers $\langle n\rangle=1/(e^t\mp 1)$ to the same log kernels. StatisticsKernels imports it to derive all four Bose/Fermi kernels from the single-mode grand partition function at $\mu=0$, discharging the MODEL status that PhaseSpaceReduction assigned them.

Together with GrandPotential, the package turns the Euler relation $T\cdot s=\rho+p$ into an explicit integral identity for massless ideal gases, which is the equilibrium input EntropyConservationFRW needs. In the broader RS forcing picture this is ordinary equilibrium statistical mechanics in $D=3$ (T8), not a new forcing step; it is the calculational bridge from per-mode $\ln Z$ to cosmological $p$ and $\rho$.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)