IndisputableMonolith.Cosmology.EntropyPerPhoton

   1import Mathlib
   2
   3/-!
   4# Entropy per Photon 7.04 from ζ(3), π⁴, and g*s = 43/11
   5
   6**Status: THEOREM (analysis + arithmetic) over MODEL inputs (Standard Model
   7particle content and Fermi–Dirac statistics).**
   8
   9This module derives the entropy-per-photon ratio used by the baryogenesis
  10dynamical lane,
  11
  12  `s / n_γ = π⁴ g*s / (45 ζ(3))  ∈ (7.0393, 7.0396)`,
  13
  14replacing the bare constant `7.04` in `EpsilonCPFromGap.dynPrefactor` with a
  15derivation. The three ingredients:
  16
  17## 1. ζ(3) window (THEOREM)
  18
  19`zeta3 := ∑ 1/(n+1)³` is bounded by splitting at 40 terms:
  20the partial sum `S40` is evaluated exactly by `norm_num`
  21(`1.2017520 < S40 < 1.2017522`), and the tail `∑_{n≥41} 1/n³` is trapped by
  22two telescoping series,
  23
  24  `1/(2(n+41)(n+42)) − 1/(2(n+42)(n+43)) = 1/((n+41)(n+42)(n+43)) ≤ 1/(n+41)³`
  25  `1/(2(n+40)(n+41)) − 1/(2(n+41)(n+42)) = 1/((n+40)(n+41)(n+42)) ≥ 1/(n+41)³`
  26
  27giving `1/3444 ≤ tail ≤ 1/3280` and hence
  28
  29  `1.202042 < ζ(3) < 1.202065`   (true value 1.2020569…).
  30
  31## 2. π⁴ window (THEOREM)
  32
  33From Mathlib's `Real.pi_gt_d6` / `Real.pi_lt_d6`:
  34`97.40900 < π⁴ < 97.40914` (true value 97.409091…).
  35
  36## 3. g*s = 43/11 (THEOREM (arithmetic) from MODEL particle content)
  37
  38Present-day entropy degrees of freedom. MODEL inputs: the photon has 2
  39polarizations; e± carry 4 fermionic dof; 3 neutrino generations carry 6
  40fermionic dof. The `7/8` fermion weight is now THEOREM, not a MODEL input:
  41`Cosmology.FermionWeight` proves the series identity `η(4) = (7/8)·ζ(4)`
  42and `Cosmology.FermionWeightIntegral` proves the thermodynamic integrals
  43themselves (`∫x³/(eˣ+1) = 7π⁴/120 = (7/8)·∫x³/(eˣ−1)`, both axiom-clean).
  44Entropy conservation through e± annihilation heats photons but not the
  45decoupled neutrinos:
  46
  47  `(T_ν/T_γ)³ = g_after/g_before = 2 / (2 + (7/8)·4) = 4/11`,
  48
  49so `g*s = 2 + (7/8)·6·(4/11) = 43/11`.
  50
  51The conservation step itself is now THEOREM, not arithmetic-by-definition:
  52`Cosmology.NeutrinoDilution` (which imports this module) derives
  53`(T_ν/T_γ)³ = 4/11` from comoving entropy conservation plus free neutrino
  54streaming, with the plasma entropy density built from the entropy-functional
  55integrals of `Cosmology.RadiationEntropyRelation` (`∫σ_B = 4π⁴/45`,
  56`∫σ_F = 7π⁴/90`, both derived), and re-derives `g*s = 43/11` as the
  57present-day total (`gStarS_from_conservation`). What stays MODEL is only
  58the particle content and the two named conservation hypotheses.
  59
  60## Result
  61
  62  `entropyPerPhoton = π⁴ (43/11) / (45 ζ(3)) ∈ (7.0393, 7.0396)`.
  63
  64The bare `7.04` used in the staging modules is this value rounded to three
  65significant figures. The bridge module `DynPrefactorDerived` propagates the
  66window into the dynamical prefactor `P = (28/79) · s/n_γ` and re-proves the
  67rung-selection theorems with the fully derived prefactor.
  68
  69Reference: Kolb & Turner, *The Early Universe*, §3.3–3.4.
  70-/
  71
  72namespace IndisputableMonolith
  73namespace Cosmology
  74namespace EntropyPerPhoton
  75
  76open Filter Topology
  77
  78/-! ## §1. g*s = 43/11 from particle content and entropy conservation -/
  79
  80/-- Photon internal dof: 2 polarizations (MODEL input). -/
  81def gPhoton : ℚ := 2
  82
  83/-- Electron–positron internal dof: 2 spin states × (e⁻ + e⁺) (MODEL input). -/
  84def gElectron : ℚ := 4
  85
  86/-- Neutrino internal dof: 3 generations × (ν + ν̄) × 1 helicity (MODEL input). -/
  87def gNeutrino : ℚ := 6
  88
  89/-- Fermionic entropy weight `7/8`: the ratio of the Fermi–Dirac to
  90Bose–Einstein thermodynamic integrals, `∫x³/(eˣ+1) / ∫x³/(eˣ−1) = η(4)/ζ(4)
  91= 1 − 2⁻³ = 7/8`.
  92
  93**THEOREM-backed** (upgraded from MODEL 2026-07-01): the series layer is
  94`FermionWeight.fermionWeight_eq_eta_zeta_ratio` (`η(4) = (7/8)·ζ(4)`), and
  95the integral layer is `FermionWeightIntegral.fermi_integral_eq_weight_mul_bose`
  96(`∫ t³/(eᵗ+1) = (7/8)·∫ t³/(eᵗ−1)`, with both integrals in closed form:
  97`π⁴/15` and `7π⁴/120`). Both are axiom-clean. The modules import this
  98definition (not vice versa), so the value stays a plain rational here. -/
  99def fermionWeight : ℚ := 7 / 8
 100
 101/-- Entropy dof of the photon–electron plasma before e± annihilation:
 102`2 + (7/8)·4 = 11/2`. -/
 103def gBefore : ℚ := gPhoton + fermionWeight * gElectron
 104
 105/-- Entropy dof of the photon sector after e± annihilation: photons only. -/
 106def gAfter : ℚ := gPhoton
 107
 108/-- **THEOREM-backed (neutrino dilution).** Entropy conservation in the
 109photon–electron sector across e± annihilation (`g·(aT)³` fixed while
 110decoupled neutrinos redshift freely) forces
 111`(T_ν/T_γ)³ = g_after/g_before = 4/11`.
 112
 113The physical derivation is `NeutrinoDilution.dilution_from_entropy_conservation`
 114(which imports this module, not vice versa): entropy conservation plus free
 115neutrino streaming force `(T_ν/T_γ)³ = 4/11`, with the plasma entropy built
 116from the derived entropy-functional integrals (`RadiationEntropyRelation`),
 117so the `11/2 → 2` dof drop is itself derived, never assumed. Here the value
 118stays a plain rational. -/
 119def dilutionCubed : ℚ := gAfter / gBefore
 120
 121theorem dilutionCubed_eq : dilutionCubed = 4 / 11 := by
 122  unfold dilutionCubed gAfter gBefore gPhoton fermionWeight gElectron
 123  norm_num
 124
 125/-- Present-day entropy degrees of freedom: photons at `T_γ` plus 3 neutrino
 126species diluted by `(T_ν/T_γ)³ = 4/11`. -/
 127def gStarS : ℚ := gPhoton + fermionWeight * gNeutrino * dilutionCubed
 128
 129/-- **THEOREM.** `g*s = 43/11 ≈ 3.909`. -/
 130theorem gStarS_eq : gStarS = 43 / 11 := by
 131  unfold gStarS gPhoton fermionWeight gNeutrino
 132  rw [dilutionCubed_eq]
 133  norm_num
 134
 135/-! ## §2. ζ(3) window
 136
 137`zeta3 = S40 + tail`. The tail `∑_{n≥0} 1/(n+41)³` is trapped between two
 138telescoping sums; `S40` is evaluated by exact rational arithmetic. -/
 139
 140/-- Apéry's constant as the series `∑_{n≥0} 1/(n+1)³`. -/
 141noncomputable def zeta3 : ℝ := ∑' n : ℕ, 1 / ((n : ℝ) + 1) ^ 3
 142
 143lemma zeta3_summable : Summable (fun n : ℕ => 1 / ((n : ℝ) + 1) ^ 3) := by
 144  have h := (Real.summable_one_div_nat_pow (p := 3)).mpr (by norm_num)
 145  have h1 := ((summable_nat_add_iff 1).mpr h)
 146  refine h1.congr fun n => ?_
 147  push_cast
 148  ring_nf
 149
 150lemma tail_summable : Summable (fun n : ℕ => 1 / ((n : ℝ) + 41) ^ 3) := by
 151  have h := (Real.summable_one_div_nat_pow (p := 3)).mpr (by norm_num)
 152  have h41 := ((summable_nat_add_iff 41).mpr h)
 153  refine h41.congr fun n => ?_
 154  push_cast
 155  ring_nf
 156
 157/-- Split ζ(3) at 40 terms. -/
 158lemma zeta3_split :
 159    zeta3 = (∑ i ∈ Finset.range 40, 1 / ((i : ℝ) + 1) ^ 3)
 160      + ∑' n : ℕ, 1 / ((n : ℝ) + 41) ^ 3 := by
 161  have h := zeta3_summable.sum_add_tsum_nat_add 40
 162  unfold zeta3
 163  rw [← h]
 164  congr 1
 165  refine tsum_congr fun n => ?_
 166  push_cast
 167  ring_nf
 168
 169/-! ### Lower telescope: `gLo n = 1/(2(n+41)(n+42))`, differences ≤ tail terms -/
 170
 171/-- Lower telescoping comparator for the ζ(3) tail. -/
 172noncomputable def gLo (n : ℕ) : ℝ := 1 / (2 * ((n : ℝ) + 41) * ((n : ℝ) + 42))
 173
 174lemma gLo_nonneg (n : ℕ) : 0 ≤ gLo n := by unfold gLo; positivity
 175
 176lemma gLo_tendsto : Tendsto gLo atTop (𝓝 0) := by
 177  apply squeeze_zero gLo_nonneg (fun n => ?_) tendsto_one_div_add_atTop_nhds_zero_nat
 178  unfold gLo
 179  have hn : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
 180  rw [div_le_div_iff₀ (by positivity) (by positivity)]
 181  nlinarith
 182
 183lemma gLo_step (n : ℕ) :
 184    gLo n - gLo (n + 1) = 1 / (((n : ℝ) + 41) * ((n : ℝ) + 42) * ((n : ℝ) + 43)) := by
 185  unfold gLo
 186  have hn : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
 187  push_cast
 188  field_simp
 189  ring
 190
 191lemma gLo_antitone (n : ℕ) : 0 ≤ gLo n - gLo (n + 1) := by
 192  rw [gLo_step]
 193  have hn : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
 194  positivity
 195
 196lemma hasSum_gLo : HasSum (fun n : ℕ => gLo n - gLo (n + 1)) (gLo 0) := by
 197  rw [hasSum_iff_tendsto_nat_of_nonneg gLo_antitone]
 198  have hps : ∀ n : ℕ, ∑ i ∈ Finset.range n, (gLo i - gLo (i + 1)) = gLo 0 - gLo n :=
 199    fun n => Finset.sum_range_sub' gLo n
 200  simp only [hps]
 201  simpa using tendsto_const_nhds.sub gLo_tendsto
 202
 203lemma term_lo (n : ℕ) : gLo n - gLo (n + 1) ≤ 1 / ((n : ℝ) + 41) ^ 3 := by
 204  rw [gLo_step]
 205  have hn : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
 206  apply one_div_le_one_div_of_le (by positivity)
 207  nlinarith
 208
 209/-- The ζ(3) tail is at least `gLo 0 = 1/3444`. -/
 210lemma tail_ge : (1 : ℝ) / 3444 ≤ ∑' n : ℕ, 1 / ((n : ℝ) + 41) ^ 3 := by
 211  have h0 : gLo 0 = 1 / 3444 := by unfold gLo; norm_num
 212  exact h0 ▸ hasSum_le term_lo hasSum_gLo tail_summable.hasSum
 213
 214/-! ### Upper telescope: `gHi n = 1/(2(n+40)(n+41))`, differences ≥ tail terms -/
 215
 216/-- Upper telescoping comparator for the ζ(3) tail. -/
 217noncomputable def gHi (n : ℕ) : ℝ := 1 / (2 * ((n : ℝ) + 40) * ((n : ℝ) + 41))
 218
 219lemma gHi_tendsto : Tendsto gHi atTop (𝓝 0) := by
 220  apply squeeze_zero (fun n => by unfold gHi; positivity) (fun n => ?_)
 221    tendsto_one_div_add_atTop_nhds_zero_nat
 222  unfold gHi
 223  have hn : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
 224  rw [div_le_div_iff₀ (by positivity) (by positivity)]
 225  nlinarith
 226
 227lemma gHi_step (n : ℕ) :
 228    gHi n - gHi (n + 1) = 1 / (((n : ℝ) + 40) * ((n : ℝ) + 41) * ((n : ℝ) + 42)) := by
 229  unfold gHi
 230  have hn : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
 231  push_cast
 232  field_simp
 233  ring
 234
 235lemma gHi_antitone (n : ℕ) : 0 ≤ gHi n - gHi (n + 1) := by
 236  rw [gHi_step]
 237  have hn : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
 238  positivity
 239
 240lemma hasSum_gHi : HasSum (fun n : ℕ => gHi n - gHi (n + 1)) (gHi 0) := by
 241  rw [hasSum_iff_tendsto_nat_of_nonneg gHi_antitone]
 242  have hps : ∀ n : ℕ, ∑ i ∈ Finset.range n, (gHi i - gHi (i + 1)) = gHi 0 - gHi n :=
 243    fun n => Finset.sum_range_sub' gHi n
 244  simp only [hps]
 245  simpa using tendsto_const_nhds.sub gHi_tendsto
 246
 247lemma term_hi (n : ℕ) : 1 / ((n : ℝ) + 41) ^ 3 ≤ gHi n - gHi (n + 1) := by
 248  rw [gHi_step]
 249  have hn : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
 250  apply one_div_le_one_div_of_le (by positivity)
 251  nlinarith
 252
 253/-- The ζ(3) tail is at most `gHi 0 = 1/3280`. -/
 254lemma tail_le : (∑' n : ℕ, 1 / ((n : ℝ) + 41) ^ 3) ≤ 1 / 3280 := by
 255  have h0 : gHi 0 = 1 / 3280 := by unfold gHi; norm_num
 256  exact h0 ▸ hasSum_le term_hi tail_summable.hasSum hasSum_gHi
 257
 258/-! ### Partial sum S40 by exact rational arithmetic -/
 259
 260lemma S40_gt :
 261    (1.2017520 : ℝ) < ∑ i ∈ Finset.range 40, 1 / ((i : ℝ) + 1) ^ 3 := by
 262  norm_num [Finset.sum_range_succ]
 263
 264lemma S40_lt :
 265    (∑ i ∈ Finset.range 40, 1 / ((i : ℝ) + 1) ^ 3) < 1.2017522 := by
 266  norm_num [Finset.sum_range_succ]
 267
 268/-! ### The ζ(3) window -/
 269
 270/-- **THEOREM.** `ζ(3) > 1.202042`. -/
 271theorem zeta3_gt : (1.202042 : ℝ) < zeta3 := by
 272  rw [zeta3_split]
 273  have h1 := S40_gt
 274  have h2 := tail_ge
 275  linarith
 276
 277/-- **THEOREM.** `ζ(3) < 1.202065`. -/
 278theorem zeta3_lt : zeta3 < (1.202065 : ℝ) := by
 279  rw [zeta3_split]
 280  have h1 := S40_lt
 281  have h2 := tail_le
 282  linarith
 283
 284theorem zeta3_pos : 0 < zeta3 := lt_trans (by norm_num) zeta3_gt
 285
 286/-! ## §3. π⁴ window from Mathlib's six-digit π bounds -/
 287
 288/-- **THEOREM.** `π⁴ > 97.40900`. -/
 289theorem pi4_gt : (97.40900 : ℝ) < Real.pi ^ 4 := by
 290  have h := Real.pi_gt_d6
 291  calc (97.40900 : ℝ) < (3.141592 : ℝ) ^ 4 := by norm_num
 292    _ < Real.pi ^ 4 := by
 293        apply pow_lt_pow_left₀ h (by norm_num)
 294        norm_num
 295
 296/-- **THEOREM.** `π⁴ < 97.40914`. -/
 297theorem pi4_lt : Real.pi ^ 4 < (97.40914 : ℝ) := by
 298  have h := Real.pi_lt_d6
 299  calc Real.pi ^ 4 < (3.141593 : ℝ) ^ 4 := by
 300        apply pow_lt_pow_left₀ h (le_of_lt Real.pi_pos)
 301        norm_num
 302    _ < (97.40914 : ℝ) := by norm_num
 303
 304/-! ## §4. The entropy-per-photon ratio -/
 305
 306/-- Entropy per photon today: `s/n_γ = π⁴ g*s / (45 ζ(3))` with
 307`g*s = 43/11`. -/
 308noncomputable def entropyPerPhoton : ℝ := Real.pi ^ 4 * (43 / 11) / (45 * zeta3)
 309
 310/-- The ratio in terms of the derived `gStarS` (the `43/11` in the definition
 311is not bare: it is `gStarS`). -/
 312theorem entropyPerPhoton_eq_formula :
 313    entropyPerPhoton = Real.pi ^ 4 * (gStarS : ℝ) / (45 * zeta3) := by
 314  rw [gStarS_eq]
 315  norm_num [entropyPerPhoton]
 316
 317/-- **THEOREM (formula provenance).** `entropyPerPhoton` is exactly the ratio
 318of the entropy density `s = (2π²/45)·g*s·T³` to the photon number density
 319`n_γ = (2ζ(3)/π²)·T³` at any temperature `T > 0`. -/
 320theorem entropyPerPhoton_eq_ratio (T : ℝ) (hT : T ≠ 0) :
 321    (2 * Real.pi ^ 2 / 45 * (gStarS : ℝ) * T ^ 3)
 322      / (2 * zeta3 / Real.pi ^ 2 * T ^ 3) = entropyPerPhoton := by
 323  rw [entropyPerPhoton_eq_formula]
 324  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
 325  have hz : zeta3 ≠ 0 := ne_of_gt zeta3_pos
 326  field_simp
 327
 328/-- **THEOREM.** `s/n_γ > 7.0393`. -/
 329theorem entropyPerPhoton_gt : (7.0393 : ℝ) < entropyPerPhoton := by
 330  have hz := zeta3_lt
 331  have hp := pi4_gt
 332  have hzpos := zeta3_pos
 333  unfold entropyPerPhoton
 334  rw [lt_div_iff₀ (by linarith : (0 : ℝ) < 45 * zeta3)]
 335  nlinarith
 336
 337/-- **THEOREM.** `s/n_γ < 7.0396`. -/
 338theorem entropyPerPhoton_lt : entropyPerPhoton < (7.0396 : ℝ) := by
 339  have hz := zeta3_gt
 340  have hp := pi4_lt
 341  have hzpos := zeta3_pos
 342  unfold entropyPerPhoton
 343  rw [div_lt_iff₀ (by linarith : (0 : ℝ) < 45 * zeta3)]
 344  nlinarith
 345
 346theorem entropyPerPhoton_pos : 0 < entropyPerPhoton :=
 347  lt_trans (by norm_num) entropyPerPhoton_gt
 348
 349/-- **THEOREM (the staged constant is the derived value to 3 s.f.).**
 350`|s/n_γ − 7.04| < 0.0007`: the bare `7.04` in the staging modules is the
 351derived ratio rounded to three significant figures. -/
 352theorem entropyPerPhoton_near_704 : |entropyPerPhoton - 7.04| < 0.0007 := by
 353  rw [abs_sub_lt_iff]
 354  constructor
 355  · linarith [entropyPerPhoton_lt]
 356  · linarith [entropyPerPhoton_gt]
 357
 358end EntropyPerPhoton
 359end Cosmology
 360end IndisputableMonolith
 361