IndisputableMonolith.Cosmology.NumberDensityIntegral

   1import Mathlib
   2import IndisputableMonolith.Cosmology.EntropyPerPhoton
   3import IndisputableMonolith.Cosmology.FermionWeightIntegral
   4
   5/-!
   6# Number-Density Integrals: `∫ t²/(eᵗ−1) = 2ζ(3)` and the 3/4 Fermion Weight
   7
   8**Status: THEOREM (integral layer, s = 3).**
   9
  10`Cosmology.FermionWeightIntegral` closed the *energy-density* integrals (the
  11Mellin transforms at `s = 4`). This module closes the *number-density* layer
  12(`s = 3`), which is the last analytic ingredient of the
  13`entropyPerPhoton_eq_ratio` formula:
  14
  15  photon number density  `n_γ = (g_γ/(2π²)) T³ ∫ t²/(eᵗ−1) dt = (2ζ(3)/π²) T³`.
  16
  17The results:
  18
  19  Bose:  `∫_{0}^{∞} t²/(eᵗ−1) dt = Γ(3)·ζ(3) = 2·ζ(3)`
  20  Fermi: `∫_{0}^{∞} t²/(eᵗ+1) dt = Γ(3)·η(3) = (3/2)·ζ(3)`,
  21
  22so the number-density fermion weight is `η(3)/ζ(3) = 1 − 2⁻² = 3/4` (the
  23companion of the 7/8 *entropy* weight; it is what dilutes fermionic *number*
  24densities, e.g. `n_ν/n_γ` per species before dilution).
  25
  26## Derivation
  27
  28Same two-step Mellin argument as the `s = 4` module, at `s = 3`:
  29
  301. **Series layer.** Split `ζ(3) = ∑ 1/n³` into even and odd parts:
  31   `∑ 1/(2k)³ = ζ(3)/8`, hence odd part `= (7/8)ζ(3)`, hence
  32   `η(3) = odd − even = (3/4)·ζ(3)`. (Here `ζ(3)` is
  33   `EntropyPerPhoton.zeta3`, the Apéry constant as a `tsum`; no closed form
  34   exists and none is needed.)
  352. **Integral layer.** `hasSum_mellin` turns the geometric expansions of the
  36   kernels (`FermionWeightIntegral.bose_series` / `fermi_series`) into
  37   Dirichlet series at `s = 3` with `Γ(3) = 2`, and uniqueness of
  38   unconditional sums evaluates both Mellin integrals.
  39
  40## Capstone
  41
  42`entropyPerPhoton_from_integrals` rewrites the whole
  43`entropyPerPhoton = π⁴·g*s/(45·ζ(3))` ratio as a ratio of the two derived
  44thermodynamic integrals: numerator `(4/3)·(∫t³/(eᵗ−1))/(2π²)·g*s` (entropy
  45density coefficient via `s = (4/3)ρ/T`), denominator
  46`g_γ·(∫t²/(eᵗ−1))/(2π²)` (photon number density coefficient). After this
  47module the only MODEL content left in the entropy-per-photon chain is the
  48particle census (`g_γ = 2`, `g_e = 4`, `g_ν = 6`) and the statistical-
  49mechanics identifications (phase-space measure, `s = (4/3)ρ/T`); every
  50analytic constant is THEOREM. All theorems here are axiom-clean.
  51-/
  52
  53namespace IndisputableMonolith
  54namespace Cosmology
  55namespace NumberDensityIntegral
  56
  57open Real MeasureTheory Set
  58open EntropyPerPhoton (zeta3 zeta3_summable zeta3_pos)
  59open FermionWeightIntegral (boseKernel fermiKernel bose_series fermi_series)
  60
  61/-! ## §1. ζ(3) as an unshifted `HasSum` (the `n = 0` term vanishes) -/
  62
  63/-- `∑_{n≥0} 1/(n+1)³ = ζ(3)`: the defining sum of `EntropyPerPhoton.zeta3`. -/
  64lemma hasSum_zeta3_shift :
  65    HasSum (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + 1) ^ 3) zeta3 := by
  66  unfold EntropyPerPhoton.zeta3
  67  exact zeta3_summable.hasSum
  68
  69/-- `∑_{n≥0} 1/n³ = ζ(3)` over all of ℕ (the `n = 0` term is `1/0 = 0`). -/
  70lemma hasSum_zeta3_unshifted :
  71    HasSum (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 3) zeta3 := by
  72  have hshift : HasSum (fun n : ℕ => (1 : ℝ) / ((n + 1 : ℕ) : ℝ) ^ 3) zeta3 :=
  73    hasSum_zeta3_shift.congr_fun fun n => by push_cast; ring
  74  have h := (hasSum_nat_add_iff
  75    (f := fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 3) 1).mp hshift
  76  simpa using h
  77
  78/-! ## §2. Series layer: η(3) = (3/4)·ζ(3) by the even/odd split -/
  79
  80/-- Pointwise identity `1/(2k)³ = (1/k³)/8`, including `k = 0` where both
  81sides are `0` (division by zero). -/
  82lemma even_term_eq :
  83    (fun k : ℕ => (1 : ℝ) / ((2 * k : ℕ) : ℝ) ^ 3)
  84      = fun k : ℕ => ((1 : ℝ) / (k : ℝ) ^ 3) / 8 := by
  85  funext k
  86  rcases Nat.eq_zero_or_pos k with hk | hk
  87  · subst hk; norm_num
  88  · have hk' : (k : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hk.ne'
  89    push_cast
  90    field_simp
  91    ring
  92
  93/-- The even-index part of `ζ(3)`: `∑_k 1/(2k)³ = ζ(3)/8`. -/
  94lemma hasSum_even :
  95    HasSum (fun k : ℕ => (1 : ℝ) / ((2 * k : ℕ) : ℝ) ^ 3) (zeta3 / 8) := by
  96  rw [even_term_eq]
  97  exact hasSum_zeta3_unshifted.div_const 8
  98
  99lemma summable_odd :
 100    Summable (fun k : ℕ => (1 : ℝ) / ((2 * k + 1 : ℕ) : ℝ) ^ 3) := by
 101  have h : Summable (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 3) :=
 102    hasSum_zeta3_unshifted.summable
 103  have hinj : Function.Injective (fun k : ℕ => 2 * k + 1) := by
 104    intro a b hab
 105    simp only at hab
 106    omega
 107  have h2 := h.comp_injective hinj
 108  exact h2.congr fun k => by simp only [Function.comp_apply]
 109
 110/-- The odd-index part of `ζ(3)`: `∑_k 1/(2k+1)³ = ζ(3)·(7/8)`, by
 111subtraction and uniqueness of unconditional sums. -/
 112lemma hasSum_odd :
 113    HasSum (fun k : ℕ => (1 : ℝ) / ((2 * k + 1 : ℕ) : ℝ) ^ 3)
 114      (zeta3 * (7 / 8)) := by
 115  obtain ⟨B, hB⟩ := summable_odd
 116  have hfull : HasSum (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 3) (zeta3 / 8 + B) :=
 117    HasSum.even_add_odd hasSum_even hB
 118  have hval : zeta3 / 8 + B = zeta3 := hfull.unique hasSum_zeta3_unshifted
 119  have hBval : B = zeta3 * (7 / 8) := by linarith
 120  exact hBval ▸ hB
 121
 122/-- Even-index terms of the alternating series are negatives of the
 123even-`ζ` terms. -/
 124lemma eta_term_even (k : ℕ) :
 125    ((-1 : ℝ)) ^ (2 * k + 1) / ((2 * k : ℕ) : ℝ) ^ 3
 126      = -((1 : ℝ) / ((2 * k : ℕ) : ℝ) ^ 3) := by
 127  rw [(odd_two_mul_add_one k).neg_one_pow]
 128  push_cast
 129  ring
 130
 131/-- Odd-index terms of the alternating series are the odd-`ζ` terms. -/
 132lemma eta_term_odd (k : ℕ) :
 133    ((-1 : ℝ)) ^ (2 * k + 1 + 1) / ((2 * k + 1 : ℕ) : ℝ) ^ 3
 134      = (1 : ℝ) / ((2 * k + 1 : ℕ) : ℝ) ^ 3 := by
 135  have heven : Even (2 * k + 1 + 1) := ⟨k + 1, by ring⟩
 136  rw [heven.neg_one_pow]
 137
 138/-- **THEOREM (η(3) as a `HasSum`).** The alternating series
 139`∑ (−1)^(n+1)/n³` converges unconditionally to `(3/4)·ζ(3)`,
 140i.e. `η(3) = (3/4)·ζ(3)`. -/
 141theorem hasSum_eta_three :
 142    HasSum (fun n : ℕ => (-1 : ℝ) ^ (n + 1) / (n : ℝ) ^ 3)
 143      (3 / 4 * zeta3) := by
 144  have he : HasSum
 145      (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1) / ((2 * k : ℕ) : ℝ) ^ 3)
 146      (-(zeta3 / 8)) := by
 147    have hfun : (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1) / ((2 * k : ℕ) : ℝ) ^ 3)
 148        = fun k : ℕ => -((1 : ℝ) / ((2 * k : ℕ) : ℝ) ^ 3) := by
 149      funext k; exact eta_term_even k
 150    rw [hfun]
 151    exact hasSum_even.neg
 152  have ho : HasSum
 153      (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1 + 1) / ((2 * k + 1 : ℕ) : ℝ) ^ 3)
 154      (zeta3 * (7 / 8)) := by
 155    have hfun : (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1 + 1) / ((2 * k + 1 : ℕ) : ℝ) ^ 3)
 156        = fun k : ℕ => (1 : ℝ) / ((2 * k + 1 : ℕ) : ℝ) ^ 3 := by
 157      funext k; exact eta_term_odd k
 158    rw [hfun]
 159    exact hasSum_odd
 160  have h := HasSum.even_add_odd
 161    (f := fun n : ℕ => (-1 : ℝ) ^ (n + 1) / (n : ℝ) ^ 3) he ho
 162  convert h using 1
 163  ring
 164
 165/-- `∑_{n≥0} (−1)ⁿ/(n+1)³ = η(3) = (3/4)·ζ(3)` (index-shifted). -/
 166lemma hasSum_eta3_shift :
 167    HasSum (fun n : ℕ => (-1 : ℝ) ^ n / ((n : ℝ) + 1) ^ 3)
 168      (3 / 4 * zeta3) := by
 169  have hbase : HasSum (fun m : ℕ => (-1 : ℝ) ^ (m + 1) / (m : ℝ) ^ 3)
 170      (3 / 4 * zeta3
 171        + ∑ i ∈ Finset.range 1, (-1 : ℝ) ^ (i + 1) / (i : ℝ) ^ 3) := by
 172    simpa using hasSum_eta_three
 173  have h := (hasSum_nat_add_iff
 174    (f := fun m : ℕ => (-1 : ℝ) ^ (m + 1) / (m : ℝ) ^ 3) 1).mpr hbase
 175  exact h.congr_fun fun n => by push_cast [pow_succ]; ring
 176
 177/-- Summability of the shifted `p`-series with real (rpow) exponent 3, as
 178required by `hasSum_mellin`. -/
 179lemma summable_shift_rpow3 :
 180    Summable (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + 1) ^ (3 : ℝ)) := by
 181  have h : Summable (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ (3 : ℝ)) :=
 182    Real.summable_one_div_nat_rpow.mpr (by norm_num)
 183  have h2 := (summable_nat_add_iff
 184    (f := fun m : ℕ => (1 : ℝ) / (m : ℝ) ^ (3 : ℝ)) 1).mpr h
 185  exact h2.congr fun n => by push_cast; ring_nf
 186
 187/-! ## §3. Mellin transforms at s = 3 -/
 188
 189/-- Mellin/Dirichlet identity for the Bose kernel at `s = 3`. -/
 190lemma hasSum_mellin_bose3 :
 191    HasSum (fun n : ℕ =>
 192        Complex.Gamma 3 * (1 : ℂ) / (((n : ℝ) + 1 : ℝ) : ℂ) ^ (3 : ℂ))
 193      (mellin boseKernel 3) := by
 194  refine hasSum_mellin (a := fun _ : ℕ => (1 : ℂ)) (p := fun n : ℕ => (n : ℝ) + 1)
 195    (F := boseKernel) (s := 3)
 196    (fun i => Or.inr (by positivity)) (by norm_num) (fun t ht => ?_) ?_
 197  · have ht' : (0 : ℝ) < t := ht
 198    have hC : HasSum (fun n : ℕ => ((Real.exp (-t) ^ (n + 1) : ℝ) : ℂ))
 199        (boseKernel t) := Complex.hasSum_ofReal.mpr (bose_series ht')
 200    refine hC.congr_fun fun n => ?_
 201    have hexp : Real.exp (-((n : ℝ) + 1) * t) = Real.exp (-t) ^ (n + 1) := by
 202      rw [← Real.exp_nat_mul]
 203      congr 1
 204      push_cast
 205      ring
 206    rw [one_mul, hexp]
 207  · simpa using summable_shift_rpow3
 208
 209/-- Mellin/Dirichlet identity for the Fermi kernel at `s = 3`. -/
 210lemma hasSum_mellin_fermi3 :
 211    HasSum (fun n : ℕ =>
 212        Complex.Gamma 3 * (-1 : ℂ) ^ n / (((n : ℝ) + 1 : ℝ) : ℂ) ^ (3 : ℂ))
 213      (mellin fermiKernel 3) := by
 214  refine hasSum_mellin (a := fun n : ℕ => (-1 : ℂ) ^ n)
 215    (p := fun n : ℕ => (n : ℝ) + 1) (F := fermiKernel) (s := 3)
 216    (fun i => Or.inr (by positivity)) (by norm_num) (fun t ht => ?_) ?_
 217  · have ht' : (0 : ℝ) < t := ht
 218    have hC : HasSum
 219        (fun n : ℕ => (((-1 : ℝ) ^ n * Real.exp (-t) ^ (n + 1) : ℝ) : ℂ))
 220        (fermiKernel t) := Complex.hasSum_ofReal.mpr (fermi_series ht')
 221    refine hC.congr_fun fun n => ?_
 222    have hexp : Real.exp (-((n : ℝ) + 1) * t) = Real.exp (-t) ^ (n + 1) := by
 223      rw [← Real.exp_nat_mul]
 224      congr 1
 225      push_cast
 226      ring
 227    rw [hexp]
 228    push_cast
 229    ring
 230  · simpa using summable_shift_rpow3
 231
 232/-! ## §4. Closed-form values -/
 233
 234/-- `Γ(3) = 2! = 2`. -/
 235lemma gamma_three : Complex.Gamma 3 = 2 := by
 236  have h := Complex.Gamma_ofNat_eq_factorial 2
 237  norm_num [Nat.factorial] at h
 238  convert h using 2
 239  norm_num
 240
 241/-- `(n+1)^(3:ℂ)` (cpow of a positive real) is the real cube, cast. -/
 242lemma cpow_shift3 (n : ℕ) :
 243    ((((n : ℝ) + 1 : ℝ)) : ℂ) ^ (3 : ℂ) = ((((n : ℝ) + 1) ^ 3 : ℝ) : ℂ) := by
 244  rw [show (3 : ℂ) = ((3 : ℕ) : ℂ) by norm_num, Complex.cpow_natCast]
 245  push_cast
 246  ring
 247
 248/-- `mellin (1/(eᵗ−1)) 3 = 2·ζ(3)` (i.e. `Γ(3)·ζ(3)`). -/
 249lemma mellin_bose3_value : mellin boseKernel 3 = ((2 * zeta3 : ℝ) : ℂ) := by
 250  refine hasSum_mellin_bose3.unique ?_
 251  have hre : HasSum (fun n : ℕ => (2 : ℝ) * ((1 : ℝ) / ((n : ℝ) + 1) ^ 3))
 252      (2 * zeta3) := hasSum_zeta3_shift.mul_left 2
 253  have hC := Complex.hasSum_ofReal.mpr hre
 254  refine hC.congr_fun fun n => ?_
 255  rw [gamma_three, cpow_shift3 n]
 256  push_cast
 257  ring
 258
 259/-- `mellin (1/(eᵗ+1)) 3 = (3/2)·ζ(3)` (i.e. `Γ(3)·η(3)`). -/
 260lemma mellin_fermi3_value : mellin fermiKernel 3 = ((3 / 2 * zeta3 : ℝ) : ℂ) := by
 261  refine hasSum_mellin_fermi3.unique ?_
 262  have hre : HasSum (fun n : ℕ => (2 : ℝ) * ((-1 : ℝ) ^ n / ((n : ℝ) + 1) ^ 3))
 263      (3 / 2 * zeta3) := by
 264    have h := hasSum_eta3_shift.mul_left 2
 265    convert h using 1
 266    ring
 267  have hC := Complex.hasSum_ofReal.mpr hre
 268  refine hC.congr_fun fun n => ?_
 269  rw [gamma_three, cpow_shift3 n]
 270  push_cast
 271  ring
 272
 273/-! ## §5. The Mellin transforms are the number-density integrals -/
 274
 275/-- `mellin boseKernel 3` is the (complexified) Bose number integral. -/
 276lemma mellin_bose3_eq_integral :
 277    mellin boseKernel 3
 278      = (((∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t - 1) : ℝ)) : ℂ) := by
 279  have h1 : mellin boseKernel 3
 280      = ∫ t in Ioi (0 : ℝ), ((t ^ 2 / (Real.exp t - 1) : ℝ) : ℂ) := by
 281    unfold mellin
 282    refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
 283    rw [smul_eq_mul, show (3 : ℂ) - 1 = ((2 : ℕ) : ℂ) by norm_num,
 284      Complex.cpow_natCast]
 285    unfold FermionWeightIntegral.boseKernel
 286    push_cast
 287    ring
 288  rw [h1, integral_complex_ofReal]
 289
 290/-- `mellin fermiKernel 3` is the (complexified) Fermi number integral. -/
 291lemma mellin_fermi3_eq_integral :
 292    mellin fermiKernel 3
 293      = (((∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t + 1) : ℝ)) : ℂ) := by
 294  have h1 : mellin fermiKernel 3
 295      = ∫ t in Ioi (0 : ℝ), ((t ^ 2 / (Real.exp t + 1) : ℝ) : ℂ) := by
 296    unfold mellin
 297    refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
 298    rw [smul_eq_mul, show (3 : ℂ) - 1 = ((2 : ℕ) : ℂ) by norm_num,
 299      Complex.cpow_natCast]
 300    unfold FermionWeightIntegral.fermiKernel
 301    push_cast
 302    ring
 303  rw [h1, integral_complex_ofReal]
 304
 305/-! ## §6. The number-density integrals in closed form -/
 306
 307/-- **THEOREM (Bose number integral).** `∫_{0}^{∞} t²/(eᵗ−1) dt = 2·ζ(3)`.
 308This is the analytic content of the photon number density
 309`n_γ = (2ζ(3)/π²)·T³`. -/
 310theorem bose_number_integral_value :
 311    (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t - 1)) = 2 * zeta3 := by
 312  have h := mellin_bose3_value
 313  rw [mellin_bose3_eq_integral] at h
 314  exact Complex.ofReal_inj.mp h
 315
 316/-- **THEOREM (Fermi number integral).** `∫_{0}^{∞} t²/(eᵗ+1) dt = (3/2)·ζ(3)`. -/
 317theorem fermi_number_integral_value :
 318    (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t + 1)) = 3 / 2 * zeta3 := by
 319  have h := mellin_fermi3_value
 320  rw [mellin_fermi3_eq_integral] at h
 321  exact Complex.ofReal_inj.mp h
 322
 323/-- **THEOREM (3/4 number-density fermion weight).** The Fermi–Dirac number
 324integral is exactly 3/4 of the Bose–Einstein one: `η(3)/ζ(3) = 1 − 2⁻² = 3/4`
 325(the companion of the 7/8 entropy weight). -/
 326theorem fermi_div_bose_number_integral :
 327    (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t + 1))
 328      / (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t - 1)) = 3 / 4 := by
 329  rw [bose_number_integral_value, fermi_number_integral_value]
 330  have hz : zeta3 ≠ 0 := zeta3_pos.ne'
 331  field_simp
 332  ring
 333
 334/-! ## §7. Capstone: the density coefficients of `entropyPerPhoton` -/
 335
 336/-- **THEOREM (photon number-density coefficient provenance).** The `2ζ(3)/π²`
 337coefficient of `n_γ = (2ζ(3)/π²)·T³` is `g_γ·(∫t²/(eᵗ−1))/(2π²)` with
 338`g_γ = 2`: the Bose number integral over the phase-space normalization. -/
 339theorem number_density_coeff_provenance :
 340    ((EntropyPerPhoton.gPhoton : ℚ) : ℝ)
 341        * (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t - 1)) / (2 * π ^ 2)
 342      = 2 * zeta3 / π ^ 2 := by
 343  rw [bose_number_integral_value]
 344  unfold EntropyPerPhoton.gPhoton
 345  have hpi : (π : ℝ) ≠ 0 := Real.pi_ne_zero
 346  push_cast
 347  field_simp
 348
 349/-- **THEOREM (entropy-density coefficient provenance).** The `2π²/45`
 350coefficient of `s = (2π²/45)·g*s·T³` is `(4/3)·(∫t³/(eᵗ−1))/(2π²)`: the
 351radiation relation `s = (4/3)ρ/T` applied to the Bose energy integral over
 352the phase-space normalization. -/
 353theorem entropy_density_coeff_provenance :
 354    4 / 3 * ((∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1)) / (2 * π ^ 2))
 355      = 2 * π ^ 2 / 45 := by
 356  rw [FermionWeightIntegral.bose_integral_value]
 357  have hpi : (π : ℝ) ≠ 0 := Real.pi_ne_zero
 358  field_simp
 359  ring
 360
 361/-- **THEOREM (entropy per photon from the thermodynamic integrals).**
 362`entropyPerPhoton` is exactly the ratio built from the two derived integrals:
 363numerator = entropy-density coefficient `(4/3)·(∫t³/(eᵗ−1))/(2π²)` times
 364`g*s`; denominator = photon number-density coefficient
 365`g_γ·(∫t²/(eᵗ−1))/(2π²)`. Every analytic constant in the entropy-per-photon
 366chain is now THEOREM; the remaining MODEL content is the particle census and
 367the statistical-mechanics identifications. -/
 368theorem entropyPerPhoton_from_integrals :
 369    EntropyPerPhoton.entropyPerPhoton
 370      = (4 / 3 * ((∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1)) / (2 * π ^ 2))
 371            * ((EntropyPerPhoton.gStarS : ℚ) : ℝ))
 372        / (((EntropyPerPhoton.gPhoton : ℚ) : ℝ)
 373            * (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t - 1)) / (2 * π ^ 2)) := by
 374  rw [FermionWeightIntegral.bose_integral_value, bose_number_integral_value,
 375    EntropyPerPhoton.gStarS_eq]
 376  unfold EntropyPerPhoton.entropyPerPhoton EntropyPerPhoton.gPhoton
 377  have hpi : (π : ℝ) ≠ 0 := Real.pi_ne_zero
 378  have hz : zeta3 ≠ 0 := zeta3_pos.ne'
 379  push_cast
 380  field_simp
 381  ring
 382
 383end NumberDensityIntegral
 384end Cosmology
 385end IndisputableMonolith
 386