IndisputableMonolith.Cosmology.PhaseSpaceReduction

   1import Mathlib
   2import IndisputableMonolith.Cosmology.GrandPotential
   3
   4/-!
   5# Phase-Space Reduction: the `g/(2π²)·T⁴` prefactor from D = 3
   6
   7## What this module derives
   8
   9`GrandPotential.plasmaPressure` and `plasmaEnergy` were *defined* in the
  101-dimensional reduced form
  11
  12  `P = (g/2π²) · T⁴ · ∫ t² K(t) dt`,
  13
  14i.e. the angular factor `4π/(2π)³ = 1/(2π²)` and the `T⁴` scaling were
  15assumed as part of the definition (MODEL).  This module derives both from
  16the underlying 3-dimensional momentum-space integral
  17
  18  `P = (g/(2π)³) · ∫ d³k  T·K(‖k‖/T)`
  19
  20using only:
  21
  22* the radial (co-area) reduction of a Haar integral of a norm-dependent
  23  function (`MeasureTheory.integral_fun_norm_addHaar`),
  24* the volume of the unit ball in ℝ³ (`4π/3`), and
  25* the substitution `k = T·t` (`integral_comp_mul_left_Ioi`).
  26
  27Both reduction theorems are **unconditional** (no integrability
  28hypotheses): the Mathlib change-of-variables lemmas hold in junk-value
  29semantics on both sides simultaneously.
  30
  31## The dimension connection (Stefan–Boltzmann exponent = D + 1)
  32
  33`phaseSpaceDensity_T_scaling` proves, for ANY spatial dimension `d ≠ 0`,
  34
  35  `P_d(T) = T^(d+1) · P_d(1)`.
  36
  37So the Stefan–Boltzmann exponent 4 is not an independent input: it is
  38`D + 1` with `D = 3`, and D = 3 is a THEOREM upstream
  39(`Foundation.UnifiedForcingChain.t8_holds`, the T8 dimension forcing).
  40`stefan_boltzmann_from_D3` instantiates this at `d = 3`.
  41
  42## Provenance ledger (honest tags)
  43
  44* THEOREM (this module): the `1/(2π²)` prefactor = (unit-ball volume
  45  `4π/3`) × (dimension 3) / (mode density `(2π)³`); the `T⁴` scaling =
  46  `T^(D+1)` at `D = 3`; the identification of the reduced integrals with
  47  `plasmaPressure`/`plasmaEnergy`.
  48* THEOREM (upstream): `D = 3` (T8); the integral values `π⁴/45`, `7π⁴/360`,
  49  `π⁴/15`, `7π⁴/120` (`RadiationEntropyRelation`, `FermionWeightIntegral`);
  50  the potential structure `s = dP/dT` (`GrandPotential`).
  51* MODEL (remaining upstream inputs): the phase-space mode density
  52  `d³k/(2π)³` per unit volume (Fourier mode counting in a box, ℏ = 1);
  53  the massless dispersion `E = ‖k‖` (c = 1).
  54* THEOREM (downstream, `StatisticsKernels`): the Bose/Fermi log kernels
  55  `∓ln(1∓e^{−E/T})` and energy kernels `t/(eᵗ∓1)` are DERIVED from the
  56  single-mode grand partition function `Σ e^{−n·E/T}` (geometric series
  57  for `n ∈ ℕ`, two-state sum for `n ∈ {0,1}`), together with the BE/FD
  58  distributions and `⟨n⟩ = −d(ln Z)/dt` consistency.
  59-/
  60
  61namespace IndisputableMonolith
  62namespace Cosmology
  63namespace PhaseSpaceReduction
  64
  65open Real MeasureTheory Set Metric
  66
  67/-! ## §1. The phase-space integral and its named kernels -/
  68
  69/-- Grand-canonical phase-space integral of one massless sector in `d`
  70spatial dimensions: degeneracy `g`, temperature `T`, dimensionless kernel
  71`K` evaluated at `E/T` with `E = ‖k‖`, and mode density `1/(2π)^d`.
  72
  73* Pressure: `K(t) = −ln(1−e^{−t})` (Bose) or `ln(1+e^{−t})` (Fermi),
  74  from `±T·ln Z` per mode.
  75* Energy density: `K(t) = t/(eᵗ∓1)`, i.e. `E·n(E/T)` per mode rescaled
  76  by `T`. -/
  77noncomputable def phaseSpaceDensity (d : ℕ) (g T : ℝ) (K : ℝ → ℝ) : ℝ :=
  78  g / (2 * π) ^ d * ∫ k : EuclideanSpace ℝ (Fin d), T * K (‖k‖ / T)
  79
  80/-- Bose pressure kernel `−ln(1−e^{−t})`. -/
  81noncomputable def boseLogKernel (t : ℝ) : ℝ := -Real.log (1 - Real.exp (-t))
  82
  83/-- Fermi pressure kernel `ln(1+e^{−t})`. -/
  84noncomputable def fermiLogKernel (t : ℝ) : ℝ := Real.log (1 + Real.exp (-t))
  85
  86/-- Bose energy kernel `t/(eᵗ−1)` (occupation number times `E/T`). -/
  87noncomputable def boseEnergyKernel (t : ℝ) : ℝ := t / (Real.exp t - 1)
  88
  89/-- Fermi energy kernel `t/(eᵗ+1)`. -/
  90noncomputable def fermiEnergyKernel (t : ℝ) : ℝ := t / (Real.exp t + 1)
  91
  92/-! ## §2. The two reduction lemmas -/
  93
  94/-- **Radial reduction in D = 3.**  A Haar integral over momentum space of
  95a function of `‖k‖` collapses to `4π ∫ y² f(y) dy`: the co-area
  96factorization (sphere × radius), with the angular factor `4π` arriving as
  97`3 × vol(B³) = 3 × (4π/3)`.  Unconditional. -/
  98theorem integral_norm_fin_three (f : ℝ → ℝ) :
  99    (∫ k : EuclideanSpace ℝ (Fin 3), f ‖k‖)
 100      = 4 * π * ∫ y in Ioi (0 : ℝ), y ^ 2 * f y := by
 101  have h := MeasureTheory.integral_fun_norm_addHaar
 102    (μ := (volume : Measure (EuclideanSpace ℝ (Fin 3)))) f
 103  simp only [finrank_euclideanSpace, Fintype.card_fin] at h
 104  have hball : (volume : Measure (EuclideanSpace ℝ (Fin 3))).real (ball 0 1)
 105      = π * 4 / 3 := by
 106    rw [measureReal_def, EuclideanSpace.volume_ball_fin_three]
 107    rw [ENNReal.ofReal_one, one_pow, one_mul,
 108      ENNReal.toReal_ofReal (by positivity)]
 109  rw [h, hball]
 110  simp only [nsmul_eq_mul, smul_eq_mul]
 111  push_cast
 112  ring
 113
 114/-- **Temperature substitution** `y = T·t`: pulls `T^(n+1)` out of a radial
 115integral with weight `yⁿ` and kernel argument `y/T`.  Unconditional. -/
 116theorem radial_scale_pow (n : ℕ) (K : ℝ → ℝ) {T : ℝ} (hT : 0 < T) :
 117    (∫ y in Ioi (0 : ℝ), y ^ n * K (y / T))
 118      = T ^ (n + 1) * ∫ t in Ioi (0 : ℝ), t ^ n * K t := by
 119  have hT0 : T ≠ 0 := ne_of_gt hT
 120  have hb : (0 : ℝ) < T⁻¹ := inv_pos.mpr hT
 121  have hsub := integral_comp_mul_left_Ioi (fun x => x ^ n * K x) 0 hb
 122  simp only [mul_zero, inv_inv, smul_eq_mul] at hsub
 123  -- hsub : ∫ x in Ioi 0, (T⁻¹*x)^n * K (T⁻¹*x) = T * ∫ x in Ioi 0, x^n * K x
 124  have hfun : (fun y : ℝ => y ^ n * K (y / T))
 125      = fun y : ℝ => T ^ n * ((T⁻¹ * y) ^ n * K (T⁻¹ * y)) := by
 126    funext y
 127    rw [inv_mul_eq_div]
 128    have hpow : T ^ n * (y / T) ^ n = y ^ n := by
 129      rw [div_pow]
 130      field_simp
 131    calc y ^ n * K (y / T)
 132        = (T ^ n * (y / T) ^ n) * K (y / T) := by rw [hpow]
 133      _ = T ^ n * ((y / T) ^ n * K (y / T)) := by ring
 134  rw [hfun, integral_const_mul, hsub]
 135  ring
 136
 137/-! ## §3. The main theorem: the 1D form with its `g/(2π²)·T⁴` prefactor -/
 138
 139/-- **THEOREM (phase-space reduction, D = 3).**  The 3-dimensional
 140grand-canonical integral reduces to the 1-dimensional form with prefactor
 141`g/(2π²) · T⁴`:
 142
 143  `(g/(2π)³) ∫ d³k T·K(‖k‖/T)  =  (g/2π²) · T⁴ · ∫ t² K(t) dt`.
 144
 145The `1/(2π²)` is `4π/(2π)³` (angular / mode density); the `T⁴` is
 146`T·T³ = T^(D+1)` from the kernel rescaling and the substitution `k = T·t`.
 147Nothing about the kernel is used: this holds for pressure, energy, entropy
 148and number-density kernels alike. -/
 149theorem phaseSpaceDensity_reduction (g : ℝ) {T : ℝ} (hT : 0 < T)
 150    (K : ℝ → ℝ) :
 151    phaseSpaceDensity 3 g T K
 152      = g / (2 * π ^ 2) * T ^ 4 * ∫ t in Ioi (0 : ℝ), t ^ 2 * K t := by
 153  unfold phaseSpaceDensity
 154  have hrad := integral_norm_fin_three (fun y => T * K (y / T))
 155  simp only [] at hrad
 156  rw [hrad]
 157  have hswap : (fun y : ℝ => y ^ 2 * (T * K (y / T)))
 158      = fun y : ℝ => T * (y ^ 2 * K (y / T)) := by
 159    funext y; ring
 160  rw [hswap, integral_const_mul, radial_scale_pow 2 K hT]
 161  have hπ : (π : ℝ) ≠ 0 := Real.pi_ne_zero
 162  field_simp
 163  ring
 164
 165/-! ## §4. The plasma pressure and energy are the reduced integrals -/
 166
 167/-- **THEOREM (pressure from phase space).**  The 3D grand-canonical
 168pressure integral with the Bose/Fermi log kernels *is* the
 169`GrandPotential.plasmaPressure` that was previously definitional: its
 170`g/(2π²)·T⁴` prefactor is now derived. -/
 171theorem plasmaPressure_from_phaseSpace (gB gF : ℝ) {T : ℝ} (hT : 0 < T) :
 172    phaseSpaceDensity 3 gB T boseLogKernel
 173      + phaseSpaceDensity 3 gF T fermiLogKernel
 174      = GrandPotential.plasmaPressure gB gF T := by
 175  rw [phaseSpaceDensity_reduction gB hT, phaseSpaceDensity_reduction gF hT]
 176  unfold GrandPotential.plasmaPressure boseLogKernel fermiLogKernel
 177  rfl
 178
 179/-- **THEOREM (energy from phase space).**  Same for the energy density:
 180the 3D integral of `E·n(E/T)` with `E = ‖k‖` is
 181`GrandPotential.plasmaEnergy`. -/
 182theorem plasmaEnergy_from_phaseSpace (gB gF : ℝ) {T : ℝ} (hT : 0 < T) :
 183    phaseSpaceDensity 3 gB T boseEnergyKernel
 184      + phaseSpaceDensity 3 gF T fermiEnergyKernel
 185      = GrandPotential.plasmaEnergy gB gF T := by
 186  rw [phaseSpaceDensity_reduction gB hT, phaseSpaceDensity_reduction gF hT]
 187  unfold GrandPotential.plasmaEnergy boseEnergyKernel fermiEnergyKernel
 188  have hB : (fun t : ℝ => t ^ 2 * (t / (Real.exp t - 1)))
 189      = fun t : ℝ => t ^ 3 / (Real.exp t - 1) := by
 190    funext t; ring
 191  have hF : (fun t : ℝ => t ^ 2 * (t / (Real.exp t + 1)))
 192      = fun t : ℝ => t ^ 3 / (Real.exp t + 1) := by
 193    funext t; ring
 194  rw [hB, hF]
 195
 196/-- **Closed form from the 3D integral.**  Chaining the reduction with the
 197Mellin-transform integral values: the phase-space pressure is
 198`(π²/90)(g_B + (7/8)g_F)·T⁴` — Stefan–Boltzmann with the fermionic `7/8`,
 199now derived end-to-end from the momentum-space integral. -/
 200theorem phaseSpacePressure_closed_form (gB gF : ℝ) {T : ℝ} (hT : 0 < T) :
 201    phaseSpaceDensity 3 gB T boseLogKernel
 202      + phaseSpaceDensity 3 gF T fermiLogKernel
 203      = π ^ 2 / 90 * (gB + 7 / 8 * gF) * T ^ 4 := by
 204  rw [plasmaPressure_from_phaseSpace gB gF hT,
 205    GrandPotential.plasmaPressure_eq]
 206
 207/-- Energy closed form: `(π²/30)(g_B + (7/8)g_F)·T⁴`. -/
 208theorem phaseSpaceEnergy_closed_form (gB gF : ℝ) {T : ℝ} (hT : 0 < T) :
 209    phaseSpaceDensity 3 gB T boseEnergyKernel
 210      + phaseSpaceDensity 3 gF T fermiEnergyKernel
 211      = π ^ 2 / 30 * (gB + 7 / 8 * gF) * T ^ 4 := by
 212  rw [plasmaEnergy_from_phaseSpace gB gF hT,
 213    GrandPotential.plasmaEnergy_eq]
 214
 215/-! ## §5. The Stefan–Boltzmann exponent is D + 1 -/
 216
 217/-- **THEOREM (T-scaling in general dimension).**  In `d ≠ 0` spatial
 218dimensions the phase-space density scales as `T^(d+1)`:
 219
 220  `P_d(T) = T^(d+1) · P_d(1)`.
 221
 222The proof never evaluates the unit-ball volume — the scaling is pure
 223dimensional analysis of the measure `d^d k` against the substitution
 224`k = T·t`.  The exponent is structural: one power of `T` per momentum
 225dimension plus one from the kernel prefactor. -/
 226theorem phaseSpaceDensity_T_scaling (d : ℕ) (hd : d ≠ 0) (g : ℝ) {T : ℝ}
 227    (hT : 0 < T) (K : ℝ → ℝ) :
 228    phaseSpaceDensity d g T K = T ^ (d + 1) * phaseSpaceDensity d g 1 K := by
 229  haveI : Nonempty (Fin d) := ⟨⟨0, Nat.pos_of_ne_zero hd⟩⟩
 230  unfold phaseSpaceDensity
 231  have h1 := MeasureTheory.integral_fun_norm_addHaar
 232    (μ := (volume : Measure (EuclideanSpace ℝ (Fin d))))
 233    (fun y => T * K (y / T))
 234  have h2 := MeasureTheory.integral_fun_norm_addHaar
 235    (μ := (volume : Measure (EuclideanSpace ℝ (Fin d))))
 236    (fun y => (1 : ℝ) * K (y / 1))
 237  simp only [finrank_euclideanSpace, Fintype.card_fin, smul_eq_mul,
 238    nsmul_eq_mul, div_one, one_mul] at h1 h2
 239  simp only [div_one, one_mul]
 240  rw [h1, h2]
 241  have hswap : (fun y : ℝ => y ^ (d - 1) * (T * K (y / T)))
 242      = fun y : ℝ => T * (y ^ (d - 1) * K (y / T)) := by
 243    funext y; ring
 244  rw [hswap, integral_const_mul, radial_scale_pow (d - 1) K hT,
 245    Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr hd)]
 246  ring
 247
 248/-- **Stefan–Boltzmann from D = 3.**  At the forced spatial dimension
 249`D = 3` (THEOREM upstream: `Foundation.UnifiedForcingChain.t8_holds`), the
 250scaling exponent is `3 + 1 = 4`.  The `T⁴` of radiation thermodynamics is
 251the dimension theorem wearing thermodynamic clothes. -/
 252theorem stefan_boltzmann_from_D3 (g : ℝ) {T : ℝ} (hT : 0 < T)
 253    (K : ℝ → ℝ) :
 254    phaseSpaceDensity 3 g T K = T ^ 4 * phaseSpaceDensity 3 g 1 K :=
 255  phaseSpaceDensity_T_scaling 3 (by norm_num) g hT K
 256
 257/-! ## §6. The potential structure now starts in momentum space -/
 258
 259/-- **Capstone: `s = dP/dT` for the phase-space pressure.**  The derivative
 260of the 3D momentum-space pressure integral is the `radiationEntropy` built
 261from the independent entropy integrals: the full chain
 262
 263  3D phase space → 1D reduction → potential `P(T)` → `s = P′` →
 264  Euler `ρ = Ts − P` → `g*s`, dilution `4/11`, `p = ρ/3`
 265
 266is now anchored at the grand-canonical momentum integral, with only the
 267mode density `1/(2π)³`, the dispersion `E = ‖k‖`, and the statistics
 268kernels remaining as upstream inputs. -/
 269theorem phaseSpacePressure_potential (gB gF : ℝ) {x : ℝ} (hx : 0 < x) :
 270    HasDerivAt
 271      (fun T => phaseSpaceDensity 3 gB T boseLogKernel
 272        + phaseSpaceDensity 3 gF T fermiLogKernel)
 273      (NeutrinoDilution.radiationEntropy gB gF x) x := by
 274  have hbase := GrandPotential.plasmaPressure_potential gB gF x
 275  apply hbase.congr_of_eventuallyEq
 276  filter_upwards [Ioi_mem_nhds hx] with T hT
 277  exact plasmaPressure_from_phaseSpace gB gF hT
 278
 279end PhaseSpaceReduction
 280end Cosmology
 281end IndisputableMonolith
 282