IndisputableMonolith.Cosmology.NeutrinoDilution

   1import Mathlib
   2import IndisputableMonolith.Cosmology.RadiationEntropyRelation
   3import IndisputableMonolith.Cosmology.EntropyPerPhoton
   4
   5/-!
   6# Neutrino Dilution (Tν/Tγ)³ = 4/11 and g*s = 43/11 from Entropy Conservation
   7
   8**Status: THEOREM (this module, 0 sorry) over two named MODEL hypotheses —
   9both now DISCHARGED downstream in `EntropyConservationFRW` (comoving entropy
  10conservation and the `1/a` redshift law are derived there from the FRW
  11continuity equation, itself derived from the two Friedmann equations, plus
  12the equilibrium identities; see `dilution_from_frw`).**
  13
  14This module closes the next MODEL element in the η_B chain.  Up to now the
  15neutrino dilution factor `(T_ν/T_γ)³ = 4/11` and the effective entropy dof
  16`g*s = 43/11` lived in `EntropyPerPhoton` as bare rational arithmetic
  17(`dilutionCubed_eq`, `gStarS_eq`): the *ratio* `gAfter/gBefore` was defined,
  18not derived.  Here both are **derived from entropy conservation through
  19e± annihilation**, with the plasma entropy density built from the
  20integrals proven in `RadiationEntropyRelation` (the entropy functional
  21`σ(x) = x²[±(1±f)ln(1±f) − f ln f]`, whose closed forms `4π⁴/45` and
  22`7π⁴/90` were derived from the Mercator/Mellin machinery — the `4/3` and
  23`7/8` factors never assumed).
  24
  25## The physical derivation
  26
  27* `radiationEntropy gB gF T` is the entropy density of a relativistic plasma
  28  with `gB` bosonic and `gF` fermionic internal dof at temperature `T`:
  29  each species contributes `(g/2π²)·T³·∫σ`, with `∫σ_B = 4π⁴/45` and
  30  `∫σ_F = 7π⁴/90` **derived**.  The single structural theorem
  31  `radiationEntropy_eq` collapses this to `(2π²/45)·(gB + (7/8)·gF)·T³`,
  32  where the `7/8` is the *entropy-layer* fermion weight.
  33
  34* **MODEL hypothesis 1 (adiabatic expansion):** comoving entropy of the
  35  electromagnetically coupled sector is conserved through e± annihilation,
  36  `s(before)·a₁³ = s(after)·a₂³`.
  37
  38* **MODEL hypothesis 2 (free streaming):** neutrinos decouple before
  39  annihilation sharing the plasma temperature, and their temperature then
  40  redshifts as `1/a`, i.e. `a·T_ν` is constant: `a₂·T_ν = a₁·T₁`.
  41
  42* **THEOREM (`dilution_from_entropy_conservation`):** these two hypotheses
  43  force `(T_ν/T_γ)³ = 4/11`.  The `11/2 → 2` drop in coupled dof is not an
  44  input: it is `radiationEntropy 2 4 T` vs `radiationEntropy 2 0 T` with
  45  the 7/8 entropy weight emerging from the derived integrals.
  46
  47* **THEOREM (`gStarS_from_conservation`):** the present-day total entropy
  48  (photons at `T_γ` + 6 fermionic neutrino dof at `T_ν`) is then exactly
  49  `(2π²/45)·(43/11)·T_γ³` — the effective dof `g*s = 43/11` of
  50  `EntropyPerPhoton.gStarS` is derived, not assumed.
  51
  52## What remains MODEL upstream
  53
  54The particle content (2 photon polarizations, 4 e± dof, 6 neutrino dof),
  55instantaneous decoupling, and the two hypotheses above.  All statistical
  56mechanics (the 7/8 entropy weight, the 4/3 law, the 2π²/45 coefficient, and
  57the 4/11 and 43/11 ratios *given* the hypotheses) is THEOREM.
  58
  59Reference: Kolb & Turner, *The Early Universe*, §3.3–3.4.
  60-/
  61
  62namespace IndisputableMonolith
  63namespace Cosmology
  64namespace NeutrinoDilution
  65
  66open Real MeasureTheory Set
  67
  68/-! ## §1. The plasma entropy density from the derived entropy functional -/
  69
  70/-- Entropy density of a relativistic plasma with `gB` bosonic and `gF`
  71fermionic internal degrees of freedom at temperature `T`, built directly
  72from the entropy-functional integrals of `RadiationEntropyRelation`:
  73each species contributes `(g/2π²)·T³·∫σ`. -/
  74noncomputable def radiationEntropy (gB gF T : ℝ) : ℝ :=
  75  gB / (2 * π ^ 2) * T ^ 3
  76      * (∫ t in Ioi (0 : ℝ), RadiationEntropyRelation.boseEntropyIntegrand t)
  77    + gF / (2 * π ^ 2) * T ^ 3
  78      * (∫ t in Ioi (0 : ℝ), RadiationEntropyRelation.fermiEntropyIntegrand t)
  79
  80/-- **THEOREM (structural form).** The plasma entropy density collapses to
  81`(2π²/45)·(gB + (7/8)·gF)·T³`, with the `2π²/45` coefficient and the `7/8`
  82entropy weight both coming from the derived integrals `∫σ_B = 4π⁴/45`,
  83`∫σ_F = 7π⁴/90` — neither is assumed. -/
  84theorem radiationEntropy_eq (gB gF T : ℝ) :
  85    radiationEntropy gB gF T = 2 * π ^ 2 / 45 * (gB + 7 / 8 * gF) * T ^ 3 := by
  86  unfold radiationEntropy
  87  rw [RadiationEntropyRelation.bose_entropy_integral_value,
  88    RadiationEntropyRelation.fermi_entropy_integral_value]
  89  have hpi : (π : ℝ) ≠ 0 := Real.pi_ne_zero
  90  field_simp
  91  ring
  92
  93/-- The photon–electron plasma before e± annihilation (2 bosonic + 4
  94fermionic dof) carries exactly `gBefore = 11/2` effective entropy dof: the
  95`11/2` of `EntropyPerPhoton.gBefore` is the functional-layer value. -/
  96theorem plasma_before_eq_gBefore (T : ℝ) :
  97    radiationEntropy ((EntropyPerPhoton.gPhoton : ℚ) : ℝ)
  98        ((EntropyPerPhoton.gElectron : ℚ) : ℝ) T
  99      = 2 * π ^ 2 / 45 * ((EntropyPerPhoton.gBefore : ℚ) : ℝ) * T ^ 3 := by
 100  rw [radiationEntropy_eq]
 101  unfold EntropyPerPhoton.gBefore EntropyPerPhoton.gPhoton
 102    EntropyPerPhoton.gElectron EntropyPerPhoton.fermionWeight
 103  push_cast
 104  ring
 105
 106/-! ## §2. The dilution theorem -/
 107
 108/-- **THEOREM (neutrino dilution from entropy conservation).**
 109If comoving entropy of the coupled photon–e± sector is conserved through
 110annihilation (`radiationEntropy 2 4 T₁ · a₁³ = radiationEntropy 2 0 T_γ · a₂³`)
 111and decoupled neutrinos redshift freely from the shared pre-annihilation
 112temperature (`a₂·T_ν = a₁·T₁`), then
 113
 114  `(T_ν/T_γ)³ = 4/11`.
 115
 116The dof drop `11/2 → 2` is not an input: it is produced by the derived
 117entropy-functional integrals inside `radiationEntropy_eq`. -/
 118theorem dilution_from_entropy_conservation
 119    {a₁ a₂ T₁ Tγ Tν : ℝ} (ha₂ : a₂ ≠ 0) (hTγ : Tγ ≠ 0)
 120    (hcons : radiationEntropy 2 4 T₁ * a₁ ^ 3 = radiationEntropy 2 0 Tγ * a₂ ^ 3)
 121    (hfree : a₂ * Tν = a₁ * T₁) :
 122    (Tν / Tγ) ^ 3 = 4 / 11 := by
 123  rw [radiationEntropy_eq, radiationEntropy_eq] at hcons
 124  have hC : (2 * π ^ 2 / 45 : ℝ) ≠ 0 := by positivity
 125  have hkey : (11 / 2 : ℝ) * (a₁ * T₁) ^ 3 = 2 * (a₂ * Tγ) ^ 3 := by
 126    have h : (2 * π ^ 2 / 45 : ℝ) * ((11 / 2) * (a₁ * T₁) ^ 3)
 127        = (2 * π ^ 2 / 45) * (2 * (a₂ * Tγ) ^ 3) := by
 128      linear_combination hcons
 129    exact mul_left_cancel₀ hC h
 130  rw [← hfree] at hkey
 131  have ha₂3 : (a₂ : ℝ) ^ 3 ≠ 0 := pow_ne_zero 3 ha₂
 132  have hTT : (11 / 2 : ℝ) * Tν ^ 3 = 2 * Tγ ^ 3 := by
 133    have h : a₂ ^ 3 * ((11 / 2 : ℝ) * Tν ^ 3) = a₂ ^ 3 * (2 * Tγ ^ 3) := by
 134      linear_combination hkey
 135    exact mul_left_cancel₀ ha₂3 h
 136  rw [div_pow, div_eq_iff (pow_ne_zero 3 hTγ)]
 137  linarith
 138
 139/-- **THEOREM (provenance).** The physically derived dilution equals the
 140arithmetic `EntropyPerPhoton.dilutionCubed = gAfter/gBefore`: the rational
 141definition upstream is the value forced by entropy conservation. -/
 142theorem dilution_eq_dilutionCubed
 143    {a₁ a₂ T₁ Tγ Tν : ℝ} (ha₂ : a₂ ≠ 0) (hTγ : Tγ ≠ 0)
 144    (hcons : radiationEntropy 2 4 T₁ * a₁ ^ 3 = radiationEntropy 2 0 Tγ * a₂ ^ 3)
 145    (hfree : a₂ * Tν = a₁ * T₁) :
 146    (Tν / Tγ) ^ 3 = ((EntropyPerPhoton.dilutionCubed : ℚ) : ℝ) := by
 147  have h4 : ((EntropyPerPhoton.dilutionCubed : ℚ) : ℝ) = 4 / 11 := by
 148    rw [EntropyPerPhoton.dilutionCubed_eq]
 149    norm_num
 150  rw [h4]
 151  exact dilution_from_entropy_conservation ha₂ hTγ hcons hfree
 152
 153/-! ## §3. g*s = 43/11 from the diluted neutrino sector -/
 154
 155/-- **THEOREM (present-day entropy).** Photons at `T_γ` plus 6 fermionic
 156neutrino dof at `T_ν` with `(T_ν/T_γ)³ = 4/11` carry total entropy
 157`(2π²/45)·(43/11)·T_γ³`. -/
 158theorem total_entropy_today
 159    {Tγ Tν : ℝ} (hTγ : Tγ ≠ 0) (hdil : (Tν / Tγ) ^ 3 = 4 / 11) :
 160    radiationEntropy 2 0 Tγ + radiationEntropy 0 6 Tν
 161      = 2 * π ^ 2 / 45 * (43 / 11) * Tγ ^ 3 := by
 162  rw [radiationEntropy_eq, radiationEntropy_eq]
 163  have hTν3 : Tν ^ 3 = 4 / 11 * Tγ ^ 3 := by
 164    rw [div_pow, div_eq_iff (pow_ne_zero 3 hTγ)] at hdil
 165    linarith
 166  rw [hTν3]
 167  ring
 168
 169/-- **THEOREM (provenance).** The present-day total equals
 170`(2π²/45)·gStarS·T_γ³` with `EntropyPerPhoton.gStarS`: the `43/11` upstream
 171is the value forced by the diluted neutrino sector. -/
 172theorem total_entropy_eq_gStarS
 173    {Tγ Tν : ℝ} (hTγ : Tγ ≠ 0) (hdil : (Tν / Tγ) ^ 3 = 4 / 11) :
 174    radiationEntropy 2 0 Tγ + radiationEntropy 0 6 Tν
 175      = 2 * π ^ 2 / 45 * ((EntropyPerPhoton.gStarS : ℚ) : ℝ) * Tγ ^ 3 := by
 176  have h : ((EntropyPerPhoton.gStarS : ℚ) : ℝ) = 43 / 11 := by
 177    rw [EntropyPerPhoton.gStarS_eq]
 178    norm_num
 179  rw [h]
 180  exact total_entropy_today hTγ hdil
 181
 182/-- **CAPSTONE.** Entropy conservation through e± annihilation plus free
 183neutrino streaming force the present-day entropy density to be
 184`(2π²/45)·(43/11)·T_γ³`: the effective dof `g*s = 43/11` entering
 185`entropyPerPhoton = π⁴·g*s/(45·ζ(3))` (and hence the η_B dynamical
 186prefactor) is **derived** from the entropy functional, not assumed. -/
 187theorem gStarS_from_conservation
 188    {a₁ a₂ T₁ Tγ Tν : ℝ} (ha₂ : a₂ ≠ 0) (hTγ : Tγ ≠ 0)
 189    (hcons : radiationEntropy 2 4 T₁ * a₁ ^ 3 = radiationEntropy 2 0 Tγ * a₂ ^ 3)
 190    (hfree : a₂ * Tν = a₁ * T₁) :
 191    radiationEntropy 2 0 Tγ + radiationEntropy 0 6 Tν
 192      = 2 * π ^ 2 / 45 * ((EntropyPerPhoton.gStarS : ℚ) : ℝ) * Tγ ^ 3 :=
 193  total_entropy_eq_gStarS hTγ
 194    (dilution_from_entropy_conservation ha₂ hTγ hcons hfree)
 195
 196end NeutrinoDilution
 197end Cosmology
 198end IndisputableMonolith
 199