Cosmology Phase Space Reduction Phase Space Energy Closed Form

The energy formula

In thermodynamics, the energy density of a gas of massless particles at temperature T is a famous result. For a gas of photons and other bosons, it is π²/30 · g_B · T⁴, where g_B counts the number of particle types. For fermions, like electrons and neutrinos, the same formula holds but with a factor of 7/8, reflecting their different statistics. The full expression, π²/30 · (g_B + 7/8 g_F) · T⁴, is the standard result for a hot, relativistic plasma.

The Recognition Science framework proves this formula from a more basic starting point. Its machine-checked library of formal theorems shows that this energy density follows from a single integral over all possible momenta of the particles. The derivation begins with a 3-dimensional momentum-space integral, which is then reduced to a simpler 1-dimensional form using a mathematical identity. This reduction is a theorem, not an assumption.

The key theorem, phaseSpaceEnergy_closed_form, states that the energy density, defined as an integral over momentum space, equals the closed-form expression π²/30 · (g_B + 7/8 g_F) · T⁴. This is a proved result in the framework's library, meaning it follows from the axioms of the system. The proof chains together the reduction of the 3D integral to 1D, and then evaluates the resulting 1D integral using known mathematical values.

This result is significant because it shows that the T⁴ scaling of the energy density is not a separate assumption. The framework proves that in any number of spatial dimensions d, the energy density scales as T^(d+1). Since the framework also proves that space has three dimensions, the exponent becomes 3+1 = 4. The famous T⁴ law of radiation is thus a consequence of the dimension of space, not an independent input.

What this theorem does not claim is that the framework has discovered a new physical law. The formula π²/30 · (g_B + 7/8 g_F) · T⁴ is a well-known result in statistical mechanics. The framework's contribution is to show that this formula can be derived from a more fundamental integral, within its own formal system. The derivation relies on standard assumptions, such as the mode density of particles in a box and the massless dispersion relation E = |k|, which are models, not theorems.

/-- Energy closed form: `(π²/30)(g_B + (7/8)g_F)·T⁴`. -/
theorem phaseSpaceEnergy_closed_form (gB gF : ℝ) {T : ℝ} (hT : 0 < T) :
    phaseSpaceDensity 3 gB T boseEnergyKernel
      + phaseSpaceDensity 3 gF T fermiEnergyKernel
      = π ^ 2 / 30 * (gB + 7 / 8 * gF) * T ^ 4 := by
  rw [plasmaEnergy_from_phaseSpace gB gF hT,
    GrandPotential.plasmaEnergy_eq]

/-- **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

/-- **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

What this page does not claim

The framework has discovered a new physical law; the formula is a known result in statistical mechanics. The derivation is independent of standard assumptions; it relies on models for mode density and dispersion. The theorem proves the value of the fine-structure constant or any other fundamental coupling.

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: