Encyclopedia Cosmology Cosmology Phase Space Reduction Phase Space Pressure Closed Form

ARTICLE 5 claims 5 theorems

Cosmology Phase Space Reduction Phase Space Pressure Closed Form

A single machine-checked theorem turns a three-dimensional momentum integral into the familiar Stefan-Boltzmann pressure law, showing why the exponent is 4.

Verify this page

The closed pressure formula

The pressure of a hot gas of massless particles, such as photons or neutrinos in the early universe, follows a famous rule: it grows as the fourth power of the temperature. In conventional physics this T⁴ behavior is the Stefan-Boltzmann law, and the proportionality constant is usually put in by hand. The Recognition Science declaration phaseSpacePressure_closed_form derives that law from a more basic starting point: the integral over all momentum directions and magnitudes in three-dimensional space.

The theorem states that for a gas with gB bosonic and gF fermionic particle types at temperature T, the pressure equals (π²/90)(gB + (7/8)gF)T⁴. The 7/8 factor is the famous fermionic suppression. The proof works by first reducing the three-dimensional integral to a one-dimensional one, using the fact that the integrand depends only on the magnitude of the momentum, not its direction. This reduction pulls out a factor of 1/(2π²) and a factor of T⁴. The remaining one-dimensional integral is then evaluated using a standard Mellin-transform identity, giving the π²/90 coefficient.

The T⁴ exponent is not an independent input. A separate theorem in the same module, phaseSpaceDensity_T_scaling, proves that in d spatial dimensions the pressure scales as T^(d+1). The exponent is structural: one power of T for each momentum dimension, plus one from the kernel prefactor. Since the framework proves the spatial dimension is 3 (a result upstream in its forcing chain), the Stefan-Boltzmann exponent 4 follows automatically. The closed form also connects to the framework's potential structure: the derivative of this pressure with respect to temperature gives the entropy density, completing a chain from momentum space to thermodynamics.

What the theorem does not claim is just as important. It does not derive the mode density 1/(2π)³ per unit volume, the massless dispersion relation E = |k|, or the Bose and Fermi statistics kernels; these remain as modeling inputs. The theorem also does not fix the value of the degeneracy factors gB and gF, which depend on the specific particle content of a theory. Finally, the result is a mathematical identity about a particular integral; it does not by itself assert that this integral describes any actual physical gas, only that if the inputs are accepted, the pressure formula follows.

THEOREM phaseSpacePressure_closed_form · IndisputableMonolith/Cosmology/PhaseSpaceReduction.lean
phaseSpacePressure_closed_form · IndisputableMonolith/Cosmology/PhaseSpaceReduction.lean:196 
/-- **Closed form from the 3D integral.**  Chaining the reduction with the
Mellin-transform integral values: the phase-space pressure is
`(π²/90)(g_B + (7/8)g_F)·T⁴` — Stefan–Boltzmann with the fermionic `7/8`,
now derived end-to-end from the momentum-space integral. -/
theorem phaseSpacePressure_closed_form (gB gF : ℝ) {T : ℝ} (hT : 0 < T) :
    phaseSpaceDensity 3 gB T boseLogKernel
      + phaseSpaceDensity 3 gF T fermiLogKernel
      = π ^ 2 / 90 * (gB + 7 / 8 * gF) * T ^ 4 := by
  rw [plasmaPressure_from_phaseSpace gB gF hT,
    GrandPotential.plasmaPressure_eq]
THEOREM phaseSpaceDensity_reduction · IndisputableMonolith/Cosmology/PhaseSpaceReduction.lean
phaseSpaceDensity_reduction · IndisputableMonolith/Cosmology/PhaseSpaceReduction.lean:139 
/-- **THEOREM (phase-space reduction, D = 3).**  The 3-dimensional
grand-canonical integral reduces to the 1-dimensional form with prefactor
`g/(2π²) · T⁴`:

  `(g/(2π)³) ∫ d³k T·K(‖k‖/T)  =  (g/2π²) · T⁴ · ∫ t² K(t) dt`.

The `1/(2π²)` is `4π/(2π)³` (angular / mode density); the `T⁴` is
`T·T³ = T^(D+1)` from the kernel rescaling and the substitution `k = T·t`.
Nothing about the kernel is used: this holds for pressure, energy, entropy
and number-density kernels alike. -/
theorem phaseSpaceDensity_reduction (g : ℝ) {T : ℝ} (hT : 0 < T)
    (K : ℝ → ℝ) :
    phaseSpaceDensity 3 g T K
      = g / (2 * π ^ 2) * T ^ 4 * ∫ t in Ioi (0 : ℝ), t ^ 2 * K t := by
  unfold phaseSpaceDensity
  have hrad := integral_norm_fin_three (fun y => T * K (y / T))
  simp only [] at hrad
  rw [hrad]
  have hswap : (fun y : ℝ => y ^ 2 * (T * K (y / T)))
      = fun y : ℝ => T * (y ^ 2 * K (y / T)) := by
    funext y; ring
  rw [hswap, integral_const_mul, radial_scale_pow 2 K hT]
  have hπ : (π : ℝ) ≠ 0 := Real.pi_ne_zero
  field_simp
  ring
THEOREM phaseSpaceDensity_T_scaling · IndisputableMonolith/Cosmology/PhaseSpaceReduction.lean
phaseSpaceDensity_T_scaling · IndisputableMonolith/Cosmology/PhaseSpaceReduction.lean:217 
/-- **THEOREM (T-scaling in general dimension).**  In `d ≠ 0` spatial
dimensions the phase-space density scales as `T^(d+1)`:

  `P_d(T) = T^(d+1) · P_d(1)`.

The proof never evaluates the unit-ball volume — the scaling is pure
dimensional analysis of the measure `d^d k` against the substitution
`k = T·t`.  The exponent is structural: one power of `T` per momentum
dimension plus one from the kernel prefactor. -/
theorem phaseSpaceDensity_T_scaling (d : ℕ) (hd : d ≠ 0) (g : ℝ) {T : ℝ}
    (hT : 0 < T) (K : ℝ → ℝ) :
    phaseSpaceDensity d g T K = T ^ (d + 1) * phaseSpaceDensity d g 1 K := by
  haveI : Nonempty (Fin d) := ⟨⟨0, Nat.pos_of_ne_zero hd⟩⟩
  unfold phaseSpaceDensity
  have h1 := MeasureTheory.integral_fun_norm_addHaar
    (μ := (volume : Measure (EuclideanSpace ℝ (Fin d))))
    (fun y => T * K (y / T))
  have h2 := MeasureTheory.integral_fun_norm_addHaar
    (μ := (volume : Measure (EuclideanSpace ℝ (Fin d))))
    (fun y => (1 : ℝ) * K (y / 1))
  simp only [finrank_euclideanSpace, Fintype.card_fin, smul_eq_mul,
    nsmul_eq_mul, div_one, one_mul] at h1 h2
  simp only [div_one, one_mul]
  rw [h1, h2]
  have hswap : (fun y : ℝ => y ^ (d - 1) * (T * K (y / T)))
      = fun y : ℝ => T * (y ^ (d - 1) * K (y / T)) := by
    funext y; ring
  rw [hswap, integral_const_mul, radial_scale_pow (d - 1) K hT,
    Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr hd)]
  ring
THEOREM stefan_boltzmann_from_D3 · IndisputableMonolith/Cosmology/PhaseSpaceReduction.lean
stefan_boltzmann_from_D3 · IndisputableMonolith/Cosmology/PhaseSpaceReduction.lean:248 
/-- **Stefan–Boltzmann from D = 3.**  At the forced spatial dimension
`D = 3` (THEOREM upstream: `Foundation.UnifiedForcingChain.t8_holds`), the
scaling exponent is `3 + 1 = 4`.  The `T⁴` of radiation thermodynamics is
the dimension theorem wearing thermodynamic clothes. -/
theorem stefan_boltzmann_from_D3 (g : ℝ) {T : ℝ} (hT : 0 < T)
    (K : ℝ → ℝ) :
    phaseSpaceDensity 3 g T K = T ^ 4 * phaseSpaceDensity 3 g 1 K :=
  phaseSpaceDensity_T_scaling 3 (by norm_num) g hT K
THEOREM phaseSpacePressure_potential · IndisputableMonolith/Cosmology/PhaseSpaceReduction.lean
phaseSpacePressure_potential · IndisputableMonolith/Cosmology/PhaseSpaceReduction.lean:259 
/-- **Capstone: `s = dP/dT` for the phase-space pressure.**  The derivative
of the 3D momentum-space pressure integral is the `radiationEntropy` built
from the independent entropy integrals: the full chain

  3D phase space → 1D reduction → potential `P(T)` → `s = P′` →
  Euler `ρ = Ts − P` → `g*s`, dilution `4/11`, `p = ρ/3`

is now anchored at the grand-canonical momentum integral, with only the
mode density `1/(2π)³`, the dispersion `E = ‖k‖`, and the statistics
kernels remaining as upstream inputs. -/
theorem phaseSpacePressure_potential (gB gF : ℝ) {x : ℝ} (hx : 0 < x) :
    HasDerivAt
      (fun T => phaseSpaceDensity 3 gB T boseLogKernel
        + phaseSpaceDensity 3 gF T fermiLogKernel)
      (NeutrinoDilution.radiationEntropy gB gF x) x := by
  have hbase := GrandPotential.plasmaPressure_potential gB gF x
  apply hbase.congr_of_eventuallyEq
  filter_upwards [Ioi_mem_nhds hx] with T hT
  exact plasmaPressure_from_phaseSpace gB gF hT

What this page does not claim

The theorem does not derive the mode density, the massless dispersion relation, or the Bose and Fermi statistics kernels. The theorem does not fix the values of the degeneracy factors gB and gF. The theorem does not assert that the integral describes any actual physical gas without accepting the modeling inputs.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/PhaseSpaceReduction.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND