IndisputableMonolith.Cosmology.FermionWeightIntegral

   1import Mathlib
   2import IndisputableMonolith.Cosmology.EntropyPerPhoton
   3import IndisputableMonolith.Cosmology.FermionWeight
   4
   5/-!
   6# The 7/8 Fermion Weight at the Integral (Thermodynamic) Layer
   7
   8**Status: THEOREM (integral layer).**
   9
  10`Cosmology.FermionWeight` derived the series identity `η(4) = (7/8)·ζ(4)`.
  11This module closes the remaining mathematical gap between that series identity
  12and the *thermodynamic* statement actually used in the entropy bookkeeping:
  13the Fermi–Dirac energy integral is 7/8 of the Bose–Einstein one,
  14
  15  `∫_{0}^{∞} t³/(eᵗ+1) dt = (7/8) · ∫_{0}^{∞} t³/(eᵗ−1) dt`,
  16
  17with both sides evaluated in closed form:
  18
  19  Bose:  `∫ t³/(eᵗ−1) = Γ(4)·ζ(4) = 6·π⁴/90 = π⁴/15`
  20  Fermi: `∫ t³/(eᵗ+1) = Γ(4)·η(4) = 6·(7/8)·π⁴/90 = 7π⁴/120`.
  21
  22## Derivation
  23
  24Both integrals are Mellin transforms at `s = 4` of geometric series in `e^{−t}`:
  25
  26  `1/(eᵗ−1) = ∑_{n≥0} e^{−(n+1)t}`,  `1/(eᵗ+1) = ∑_{n≥0} (−1)ⁿ e^{−(n+1)t}`  (t > 0),
  27
  28and Mathlib's `hasSum_mellin` ("Mellin transform of a power series in exp(−t)
  29is a Dirichlet series") gives
  30
  31  `mellin F s = ∑_n Γ(s)·aₙ/(n+1)^s`
  32
  33for `F t = ∑ aₙ e^{−(n+1)t}`. At `s = 4` with `Γ(4) = 3! = 6`, the Dirichlet
  34sides are the shifted `ζ(4)` and `η(4)` sums evaluated in
  35`Cosmology.FermionWeight`. The Mellin integrand `t³·F(t)` is exactly the
  36thermodynamic integrand, so uniqueness of unconditional sums closes both
  37integrals, and the 7/8 ratio follows.
  38
  39With this module the *entire mathematical content* of
  40`EntropyPerPhoton.fermionWeight = 7/8` is THEOREM: the only MODEL content left
  41in the entropy-per-photon chain is the physics bookkeeping (which species are
  42relativistic, i.e. the `g*` census), not the 7/8 statistics factor itself.
  43All theorems here are axiom-clean (Lean's base three only).
  44-/
  45
  46namespace IndisputableMonolith
  47namespace Cosmology
  48namespace FermionWeightIntegral
  49
  50open Real MeasureTheory Set
  51
  52/-- The Bose–Einstein kernel `1/(eᵗ−1)`, complex-valued for the Mellin machinery. -/
  53noncomputable def boseKernel (t : ℝ) : ℂ := ((1 / (Real.exp t - 1) : ℝ) : ℂ)
  54
  55/-- The Fermi–Dirac kernel `1/(eᵗ+1)`, complex-valued for the Mellin machinery. -/
  56noncomputable def fermiKernel (t : ℝ) : ℂ := ((1 / (Real.exp t + 1) : ℝ) : ℂ)
  57
  58/-! ## §1. Geometric-series expansions of the kernels (t > 0) -/
  59
  60/-- `1/(eᵗ−1) = ∑_{n≥0} (e^{−t})^{n+1}` for `t > 0`. -/
  61lemma bose_series {t : ℝ} (ht : 0 < t) :
  62    HasSum (fun n : ℕ => Real.exp (-t) ^ (n + 1)) (1 / (Real.exp t - 1)) := by
  63  have hr0 : (0 : ℝ) ≤ Real.exp (-t) := (Real.exp_pos _).le
  64  have hr1 : Real.exp (-t) < 1 := Real.exp_lt_one_iff.mpr (by linarith)
  65  have h := (hasSum_geometric_of_lt_one hr0 hr1).mul_left (Real.exp (-t))
  66  have hval : Real.exp (-t) * (1 - Real.exp (-t))⁻¹ = 1 / (Real.exp t - 1) := by
  67    have h1 : (1 : ℝ) < Real.exp t := by
  68      rw [← Real.exp_zero]
  69      exact Real.exp_lt_exp.mpr ht
  70    have hne : Real.exp t - 1 ≠ 0 := by linarith
  71    have hne2 : (1 : ℝ) - Real.exp (-t) ≠ 0 := by linarith
  72    have hepos : Real.exp t ≠ 0 := (Real.exp_pos t).ne'
  73    rw [Real.exp_neg]
  74    rw [Real.exp_neg] at hne2
  75    field_simp
  76  exact (hval ▸ h).congr_fun fun n => by rw [pow_succ]; ring
  77
  78/-- `1/(eᵗ+1) = ∑_{n≥0} (−1)ⁿ (e^{−t})^{n+1}` for `t > 0`. -/
  79lemma fermi_series {t : ℝ} (ht : 0 < t) :
  80    HasSum (fun n : ℕ => (-1 : ℝ) ^ n * Real.exp (-t) ^ (n + 1))
  81      (1 / (Real.exp t + 1)) := by
  82  have hr0 : (0 : ℝ) < Real.exp (-t) := Real.exp_pos _
  83  have hr1 : Real.exp (-t) < 1 := Real.exp_lt_one_iff.mpr (by linarith)
  84  have hnorm : ‖-Real.exp (-t)‖ < 1 := by
  85    rw [norm_neg, Real.norm_eq_abs, abs_of_pos hr0]
  86    exact hr1
  87  have h := (hasSum_geometric_of_norm_lt_one hnorm).mul_left (Real.exp (-t))
  88  have hval : Real.exp (-t) * (1 - -Real.exp (-t))⁻¹ = 1 / (Real.exp t + 1) := by
  89    have hepos : Real.exp t ≠ 0 := (Real.exp_pos t).ne'
  90    have hne : Real.exp t + 1 ≠ 0 := by positivity
  91    have hne2 : (1 : ℝ) - -Real.exp (-t) ≠ 0 := by
  92      rw [sub_neg_eq_add]
  93      positivity
  94    rw [sub_neg_eq_add, Real.exp_neg]
  95    rw [sub_neg_eq_add, Real.exp_neg] at hne2
  96    field_simp
  97  exact (hval ▸ h).congr_fun fun n => by rw [neg_pow, pow_succ]; ring
  98
  99/-! ## §2. Shifted Dirichlet sums (from `Cosmology.FermionWeight`) -/
 100
 101/-- `∑_{n≥0} 1/(n+1)⁴ = ζ(4) = π⁴/90` (index-shifted `hasSum_zeta_four`). -/
 102lemma hasSum_zeta_shift :
 103    HasSum (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + 1) ^ 4) (π ^ 4 / 90) := by
 104  have hbase : HasSum (fun m : ℕ => (1 : ℝ) / (m : ℝ) ^ 4)
 105      (π ^ 4 / 90 + ∑ i ∈ Finset.range 1, (1 : ℝ) / (i : ℝ) ^ 4) := by
 106    simpa using hasSum_zeta_four
 107  have h := (hasSum_nat_add_iff
 108    (f := fun m : ℕ => (1 : ℝ) / (m : ℝ) ^ 4) 1).mpr hbase
 109  exact h.congr_fun fun n => by push_cast; ring
 110
 111/-- `∑_{n≥0} (−1)ⁿ/(n+1)⁴ = η(4) = (7/8)·(π⁴/90)` (index-shifted
 112`FermionWeight.hasSum_eta_four`). -/
 113lemma hasSum_eta_shift :
 114    HasSum (fun n : ℕ => (-1 : ℝ) ^ n / ((n : ℝ) + 1) ^ 4)
 115      (7 / 8 * (π ^ 4 / 90)) := by
 116  have hbase : HasSum (fun m : ℕ => (-1 : ℝ) ^ (m + 1) / (m : ℝ) ^ 4)
 117      (7 / 8 * (π ^ 4 / 90)
 118        + ∑ i ∈ Finset.range 1, (-1 : ℝ) ^ (i + 1) / (i : ℝ) ^ 4) := by
 119    simpa using FermionWeight.hasSum_eta_four
 120  have h := (hasSum_nat_add_iff
 121    (f := fun m : ℕ => (-1 : ℝ) ^ (m + 1) / (m : ℝ) ^ 4) 1).mpr hbase
 122  exact h.congr_fun fun n => by push_cast [pow_succ]; ring
 123
 124/-- Summability of the shifted `p`-series with real (rpow) exponent, as
 125required by `hasSum_mellin`. -/
 126lemma summable_shift_rpow :
 127    Summable (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + 1) ^ (4 : ℝ)) := by
 128  have h : Summable (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ (4 : ℝ)) :=
 129    Real.summable_one_div_nat_rpow.mpr (by norm_num)
 130  have h2 := (summable_nat_add_iff
 131    (f := fun m : ℕ => (1 : ℝ) / (m : ℝ) ^ (4 : ℝ)) 1).mpr h
 132  exact h2.congr fun n => by push_cast; ring_nf
 133
 134/-! ## §3. Mellin transforms at s = 4 -/
 135
 136/-- Mellin/Dirichlet identity for the Bose kernel at `s = 4`. -/
 137lemma hasSum_mellin_bose :
 138    HasSum (fun n : ℕ =>
 139        Complex.Gamma 4 * (1 : ℂ) / (((n : ℝ) + 1 : ℝ) : ℂ) ^ (4 : ℂ))
 140      (mellin boseKernel 4) := by
 141  refine hasSum_mellin (a := fun _ : ℕ => (1 : ℂ)) (p := fun n : ℕ => (n : ℝ) + 1)
 142    (F := boseKernel) (s := 4)
 143    (fun i => Or.inr (by positivity)) (by norm_num) (fun t ht => ?_) ?_
 144  · -- geometric series, cast to ℂ
 145    have ht' : (0 : ℝ) < t := ht
 146    have hC : HasSum (fun n : ℕ => ((Real.exp (-t) ^ (n + 1) : ℝ) : ℂ))
 147        (boseKernel t) := Complex.hasSum_ofReal.mpr (bose_series ht')
 148    refine hC.congr_fun fun n => ?_
 149    have hexp : Real.exp (-((n : ℝ) + 1) * t) = Real.exp (-t) ^ (n + 1) := by
 150      rw [← Real.exp_nat_mul]
 151      congr 1
 152      push_cast
 153      ring
 154    rw [one_mul, hexp]
 155  · simpa using summable_shift_rpow
 156
 157/-- Mellin/Dirichlet identity for the Fermi kernel at `s = 4`. -/
 158lemma hasSum_mellin_fermi :
 159    HasSum (fun n : ℕ =>
 160        Complex.Gamma 4 * (-1 : ℂ) ^ n / (((n : ℝ) + 1 : ℝ) : ℂ) ^ (4 : ℂ))
 161      (mellin fermiKernel 4) := by
 162  refine hasSum_mellin (a := fun n : ℕ => (-1 : ℂ) ^ n)
 163    (p := fun n : ℕ => (n : ℝ) + 1) (F := fermiKernel) (s := 4)
 164    (fun i => Or.inr (by positivity)) (by norm_num) (fun t ht => ?_) ?_
 165  · have ht' : (0 : ℝ) < t := ht
 166    have hC : HasSum
 167        (fun n : ℕ => (((-1 : ℝ) ^ n * Real.exp (-t) ^ (n + 1) : ℝ) : ℂ))
 168        (fermiKernel t) := Complex.hasSum_ofReal.mpr (fermi_series ht')
 169    refine hC.congr_fun fun n => ?_
 170    have hexp : Real.exp (-((n : ℝ) + 1) * t) = Real.exp (-t) ^ (n + 1) := by
 171      rw [← Real.exp_nat_mul]
 172      congr 1
 173      push_cast
 174      ring
 175    rw [hexp]
 176    push_cast
 177    ring
 178  · simpa using summable_shift_rpow
 179
 180/-! ## §4. Closed-form values -/
 181
 182/-- `Γ(4) = 3! = 6`. -/
 183lemma gamma_four : Complex.Gamma 4 = 6 := by
 184  have h := Complex.Gamma_ofNat_eq_factorial 3
 185  norm_num [Nat.factorial] at h
 186  convert h using 2
 187  norm_num
 188
 189/-- `(n+1)^(4:ℂ)` (cpow of a positive real) is the real fourth power, cast. -/
 190lemma cpow_shift (n : ℕ) :
 191    ((((n : ℝ) + 1 : ℝ)) : ℂ) ^ (4 : ℂ) = ((((n : ℝ) + 1) ^ 4 : ℝ) : ℂ) := by
 192  rw [show (4 : ℂ) = ((4 : ℕ) : ℂ) by norm_num, Complex.cpow_natCast]
 193  push_cast
 194  ring
 195
 196/-- `mellin (1/(eᵗ−1)) 4 = π⁴/15` (i.e. `Γ(4)·ζ(4)`). -/
 197lemma mellin_bose_value : mellin boseKernel 4 = ((π ^ 4 / 15 : ℝ) : ℂ) := by
 198  refine hasSum_mellin_bose.unique ?_
 199  have hre : HasSum (fun n : ℕ => (6 : ℝ) * ((1 : ℝ) / ((n : ℝ) + 1) ^ 4))
 200      (π ^ 4 / 15) := by
 201    have h := hasSum_zeta_shift.mul_left 6
 202    convert h using 1
 203    ring
 204  have hC := Complex.hasSum_ofReal.mpr hre
 205  refine hC.congr_fun fun n => ?_
 206  rw [gamma_four, cpow_shift n]
 207  push_cast
 208  ring
 209
 210/-- `mellin (1/(eᵗ+1)) 4 = 7π⁴/120` (i.e. `Γ(4)·η(4)`). -/
 211lemma mellin_fermi_value : mellin fermiKernel 4 = ((7 * π ^ 4 / 120 : ℝ) : ℂ) := by
 212  refine hasSum_mellin_fermi.unique ?_
 213  have hre : HasSum (fun n : ℕ => (6 : ℝ) * ((-1 : ℝ) ^ n / ((n : ℝ) + 1) ^ 4))
 214      (7 * π ^ 4 / 120) := by
 215    have h := hasSum_eta_shift.mul_left 6
 216    convert h using 1
 217    ring
 218  have hC := Complex.hasSum_ofReal.mpr hre
 219  refine hC.congr_fun fun n => ?_
 220  rw [gamma_four, cpow_shift n]
 221  push_cast
 222  ring
 223
 224/-! ## §5. The Mellin transforms are the thermodynamic integrals -/
 225
 226/-- `mellin boseKernel 4` is the (complexified) Bose–Einstein integral. -/
 227lemma mellin_bose_eq_integral :
 228    mellin boseKernel 4
 229      = (((∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1) : ℝ)) : ℂ) := by
 230  have h1 : mellin boseKernel 4
 231      = ∫ t in Ioi (0 : ℝ), ((t ^ 3 / (Real.exp t - 1) : ℝ) : ℂ) := by
 232    unfold mellin
 233    refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
 234    rw [smul_eq_mul, show (4 : ℂ) - 1 = ((3 : ℕ) : ℂ) by norm_num,
 235      Complex.cpow_natCast]
 236    unfold boseKernel
 237    push_cast
 238    ring
 239  rw [h1, integral_complex_ofReal]
 240
 241/-- `mellin fermiKernel 4` is the (complexified) Fermi–Dirac integral. -/
 242lemma mellin_fermi_eq_integral :
 243    mellin fermiKernel 4
 244      = (((∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t + 1) : ℝ)) : ℂ) := by
 245  have h1 : mellin fermiKernel 4
 246      = ∫ t in Ioi (0 : ℝ), ((t ^ 3 / (Real.exp t + 1) : ℝ) : ℂ) := by
 247    unfold mellin
 248    refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
 249    rw [smul_eq_mul, show (4 : ℂ) - 1 = ((3 : ℕ) : ℂ) by norm_num,
 250      Complex.cpow_natCast]
 251    unfold fermiKernel
 252    push_cast
 253    ring
 254  rw [h1, integral_complex_ofReal]
 255
 256/-! ## §6. The thermodynamic integrals in closed form -/
 257
 258/-- **THEOREM (Bose–Einstein integral).** `∫_{0}^{∞} t³/(eᵗ−1) dt = π⁴/15`. -/
 259theorem bose_integral_value :
 260    (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1)) = π ^ 4 / 15 := by
 261  have h := mellin_bose_value
 262  rw [mellin_bose_eq_integral] at h
 263  exact Complex.ofReal_inj.mp h
 264
 265/-- **THEOREM (Fermi–Dirac integral).** `∫_{0}^{∞} t³/(eᵗ+1) dt = 7π⁴/120`. -/
 266theorem fermi_integral_value :
 267    (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t + 1)) = 7 * π ^ 4 / 120 := by
 268  have h := mellin_fermi_value
 269  rw [mellin_fermi_eq_integral] at h
 270  exact Complex.ofReal_inj.mp h
 271
 272/-! ## §7. Capstone: the 7/8 weight is the integral ratio -/
 273
 274/-- **THEOREM (7/8 at the thermodynamic layer).** The Fermi–Dirac energy
 275integral is exactly 7/8 of the Bose–Einstein one. -/
 276theorem fermi_div_bose_integral :
 277    (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t + 1))
 278      / (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1)) = 7 / 8 := by
 279  rw [bose_integral_value, fermi_integral_value]
 280  rw [div_eq_iff (by positivity)]
 281  ring
 282
 283/-- **THEOREM (fermion weight provenance, integral layer).** The `7/8` MODEL
 284constant of `EntropyPerPhoton.fermionWeight` is the ratio of the actual
 285thermodynamic integrals: `∫ t³/(eᵗ+1) = fermionWeight · ∫ t³/(eᵗ−1)`.
 286Together with `FermionWeight.fermionWeight_eq_eta_zeta_ratio` (series layer)
 287this makes the full mathematical content of the 7/8 factor THEOREM; the
 288remaining MODEL content of the entropy chain is the relativistic-species
 289census (`g*`), not the statistics factor. -/
 290theorem fermi_integral_eq_weight_mul_bose :
 291    (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t + 1))
 292      = ((EntropyPerPhoton.fermionWeight : ℚ) : ℝ)
 293          * ∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1) := by
 294  rw [bose_integral_value, fermi_integral_value]
 295  unfold EntropyPerPhoton.fermionWeight
 296  push_cast
 297  ring
 298
 299end FermionWeightIntegral
 300end Cosmology
 301end IndisputableMonolith
 302