IndisputableMonolith.Cosmology.FermionWeight

   1import Mathlib
   2import IndisputableMonolith.Cosmology.EntropyPerPhoton
   3
   4/-!
   5# The 7/8 Fermion Entropy Weight from the Eta/Zeta Series Identity
   6
   7**Status: THEOREM (series layer).**
   8
   9This module upgrades the `fermionWeight = 7/8` MODEL input of
  10`Cosmology.EntropyPerPhoton` to a derived identity at the series level:
  11
  12  `η(4) = (7/8) · ζ(4)`,
  13
  14where `ζ(4) = ∑ 1/n⁴ = π⁴/90` (Mathlib's `hasSum_zeta_four`) and
  15`η(4) = ∑ (−1)^(n+1)/n⁴` is the Dirichlet eta value that controls the
  16Fermi–Dirac thermodynamic integral `∫ x³/(eˣ+1) dx = Γ(4)·η(4)` (the
  17Bose–Einstein integral being `∫ x³/(eˣ−1) dx = Γ(4)·ζ(4)`; the integral
  18layer lives in `Cosmology.FermionWeightIntegral`).
  19
  20## Derivation
  21
  22Split `ζ(4)` into even- and odd-index parts:
  23
  24  even: `∑ 1/(2k)⁴ = (1/16)·ζ(4)`   (n = 2k re-indexing, k = 0 term vanishes)
  25  odd:  `∑ 1/(2k+1)⁴ = (15/16)·ζ(4)` (by subtraction and uniqueness of sums)
  26
  27Then the alternating series is odd-part minus even-part:
  28
  29  `η(4) = (15/16)·ζ(4) − (1/16)·ζ(4) = (14/16)·ζ(4) = (7/8)·ζ(4)`.
  30
  31All sums are unconditional (`HasSum` over ℕ); the even/odd recombination is
  32Mathlib's `HasSum.even_add_odd`; no axioms beyond Lean's base three.
  33
  34The final theorem `fermionWeight_eq_eta_zeta_ratio` states that the rational
  35`7/8` used in `EntropyPerPhoton.fermionWeight` is exactly `η(4)/ζ(4)`, which
  36removes "the eta/zeta series identity is classical" from the MODEL-input list
  37(the remaining MODEL content of the weight is only the *statistical mechanics*
  38statement that a fermion species contributes the Fermi–Dirac integral, i.e.
  39the physics input, not the mathematics).
  40-/
  41
  42namespace IndisputableMonolith
  43namespace Cosmology
  44namespace FermionWeight
  45
  46open Real
  47
  48/-! ## §1. Even part: `∑ 1/(2k)⁴ = ζ(4)/16` -/
  49
  50/-- Pointwise identity `1/(2k)⁴ = (1/k⁴)/16`, including `k = 0` where both
  51sides are `0` (division by zero). -/
  52lemma even_term_eq :
  53    (fun k : ℕ => (1 : ℝ) / ((2 * k : ℕ) : ℝ) ^ 4)
  54      = fun k : ℕ => ((1 : ℝ) / (k : ℝ) ^ 4) / 16 := by
  55  funext k
  56  rcases Nat.eq_zero_or_pos k with hk | hk
  57  · subst hk; norm_num
  58  · have hk' : (k : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hk.ne'
  59    push_cast
  60    field_simp
  61    ring
  62
  63/-- The even-index part of `ζ(4)`: `∑_k 1/(2k)⁴ = (π⁴/90)/16`. -/
  64lemma hasSum_even :
  65    HasSum (fun k : ℕ => (1 : ℝ) / ((2 * k : ℕ) : ℝ) ^ 4) (π ^ 4 / 90 / 16) := by
  66  rw [even_term_eq]
  67  exact hasSum_zeta_four.div_const 16
  68
  69/-! ## §2. Odd part: `∑ 1/(2k+1)⁴ = (15/16)·ζ(4)` -/
  70
  71lemma summable_odd :
  72    Summable (fun k : ℕ => (1 : ℝ) / ((2 * k + 1 : ℕ) : ℝ) ^ 4) := by
  73  have h : Summable (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 4) := hasSum_zeta_four.summable
  74  have hinj : Function.Injective (fun k : ℕ => 2 * k + 1) := by
  75    intro a b hab
  76    simp only at hab
  77    omega
  78  have h2 := h.comp_injective hinj
  79  exact h2.congr fun k => by simp only [Function.comp_apply]
  80
  81/-- The odd-index part of `ζ(4)`: `∑_k 1/(2k+1)⁴ = (π⁴/90)·(15/16)`.
  82Derived by subtraction: full sum minus even part, using uniqueness of
  83unconditional sums in ℝ. -/
  84lemma hasSum_odd :
  85    HasSum (fun k : ℕ => (1 : ℝ) / ((2 * k + 1 : ℕ) : ℝ) ^ 4)
  86      (π ^ 4 / 90 * (15 / 16)) := by
  87  obtain ⟨B, hB⟩ := summable_odd
  88  have hfull : HasSum (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 4) (π ^ 4 / 90 / 16 + B) :=
  89    HasSum.even_add_odd hasSum_even hB
  90  have hval : π ^ 4 / 90 / 16 + B = π ^ 4 / 90 := hfull.unique hasSum_zeta_four
  91  have hBval : B = π ^ 4 / 90 * (15 / 16) := by linarith
  92  exact hBval ▸ hB
  93
  94/-! ## §3. The alternating (eta) series -/
  95
  96/-- Even-index terms of the alternating series are negatives of the
  97even-`ζ` terms: `(−1)^(2k+1)/(2k)⁴ = −1/(2k)⁴`. -/
  98lemma eta_term_even (k : ℕ) :
  99    ((-1 : ℝ)) ^ (2 * k + 1) / ((2 * k : ℕ) : ℝ) ^ 4
 100      = -((1 : ℝ) / ((2 * k : ℕ) : ℝ) ^ 4) := by
 101  rw [(odd_two_mul_add_one k).neg_one_pow]
 102  push_cast
 103  ring
 104
 105/-- Odd-index terms of the alternating series are the odd-`ζ` terms:
 106`(−1)^(2k+2)/(2k+1)⁴ = 1/(2k+1)⁴`. -/
 107lemma eta_term_odd (k : ℕ) :
 108    ((-1 : ℝ)) ^ (2 * k + 1 + 1) / ((2 * k + 1 : ℕ) : ℝ) ^ 4
 109      = (1 : ℝ) / ((2 * k + 1 : ℕ) : ℝ) ^ 4 := by
 110  have heven : Even (2 * k + 1 + 1) := ⟨k + 1, by ring⟩
 111  rw [heven.neg_one_pow]
 112
 113/-- **THEOREM (η(4) as a `HasSum`).** The alternating series
 114`∑ (−1)^(n+1)/n⁴` converges unconditionally to `(7/8)·(π⁴/90)`,
 115i.e. `η(4) = (7/8)·ζ(4)`. -/
 116theorem hasSum_eta_four :
 117    HasSum (fun n : ℕ => (-1 : ℝ) ^ (n + 1) / (n : ℝ) ^ 4)
 118      (7 / 8 * (π ^ 4 / 90)) := by
 119  have he : HasSum
 120      (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1) / ((2 * k : ℕ) : ℝ) ^ 4)
 121      (-(π ^ 4 / 90 / 16)) := by
 122    have hfun : (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1) / ((2 * k : ℕ) : ℝ) ^ 4)
 123        = fun k : ℕ => -((1 : ℝ) / ((2 * k : ℕ) : ℝ) ^ 4) := by
 124      funext k; exact eta_term_even k
 125    rw [hfun]
 126    exact hasSum_even.neg
 127  have ho : HasSum
 128      (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1 + 1) / ((2 * k + 1 : ℕ) : ℝ) ^ 4)
 129      (π ^ 4 / 90 * (15 / 16)) := by
 130    have hfun : (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1 + 1) / ((2 * k + 1 : ℕ) : ℝ) ^ 4)
 131        = fun k : ℕ => (1 : ℝ) / ((2 * k + 1 : ℕ) : ℝ) ^ 4 := by
 132      funext k; exact eta_term_odd k
 133    rw [hfun]
 134    exact hasSum_odd
 135  have h := HasSum.even_add_odd
 136    (f := fun n : ℕ => (-1 : ℝ) ^ (n + 1) / (n : ℝ) ^ 4) he ho
 137  convert h using 1
 138  ring
 139
 140/-- **THEOREM (the eta/zeta ratio).** `η(4) / ζ(4) = 7/8` as real numbers. -/
 141theorem eta4_div_zeta4 :
 142    (∑' n : ℕ, (-1 : ℝ) ^ (n + 1) / (n : ℝ) ^ 4)
 143      / (∑' n : ℕ, (1 : ℝ) / (n : ℝ) ^ 4) = 7 / 8 := by
 144  rw [hasSum_eta_four.tsum_eq, hasSum_zeta_four.tsum_eq]
 145  have hz : (π : ℝ) ^ 4 / 90 ≠ 0 := by positivity
 146  rw [mul_div_assoc, div_self hz, mul_one]
 147
 148/-- **THEOREM (fermion weight provenance).** The `7/8` MODEL constant in
 149`EntropyPerPhoton.fermionWeight` is exactly the eta/zeta ratio:
 150`fermionWeight · ζ(4) = η(4)`. The series identity is now derived, not
 151imported; the remaining MODEL content of the weight is only the
 152statistical-mechanics identification of the fermionic entropy integral. -/
 153theorem fermionWeight_eq_eta_zeta_ratio :
 154    ((EntropyPerPhoton.fermionWeight : ℚ) : ℝ)
 155        * ∑' n : ℕ, (1 : ℝ) / (n : ℝ) ^ 4
 156      = ∑' n : ℕ, (-1 : ℝ) ^ (n + 1) / (n : ℝ) ^ 4 := by
 157  rw [hasSum_eta_four.tsum_eq, hasSum_zeta_four.tsum_eq]
 158  unfold EntropyPerPhoton.fermionWeight
 159  push_cast
 160  ring
 161
 162end FermionWeight
 163end Cosmology
 164end IndisputableMonolith
 165