IndisputableMonolith.Cosmology.EntropyConservationFRW

   1import Mathlib
   2import IndisputableMonolith.Cosmology.NeutrinoDilution
   3
   4/-!
   5# Entropy Conservation from the FRW Continuity Equation
   6
   7**Status: THEOREM (this module, 0 sorry).**
   8
   9This module discharges the two MODEL hypotheses that `NeutrinoDilution` was
  10stated over.  There, `(T_ν/T_γ)³ = 4/11` and `g*s = 43/11` were derived from
  11
  12* **adiabatic expansion** — comoving entropy `s·a³` of the coupled sector is
  13  conserved through e± annihilation, and
  14* **free streaming** — the decoupled neutrino temperature redshifts as `1/a`
  15  (`a·T_ν` constant),
  16
  17both *assumed*.  Here both are **derived**:
  18
  19## The derivation chain
  20
  21* **§0 (`continuity_from_friedmann`).** The FRW continuity equation
  22  `a·ρ′ = −3a′(ρ+p)` is itself not an axiom: it is forced by the two
  23  Friedmann equations `a′² = (8πG/3)ρa²` and `a″a = −(4πG/3)(ρ+3p)a²`
  24  (differentiate the first, substitute the second, cancel `(8πG/3)a²`).
  25  This is the Bianchi-identity compatibility of the Einstein equations,
  26  done with `HasDerivAt` and no division.
  27
  28* **§1 (`comoving_entropy_conserved`).** For any fluid in local equilibrium —
  29  Euler relation `T·s = ρ + p` (zero chemical potential) and Gibbs–Duhem
  30  `p′ = s·T′` — the continuity equation forces `d/dt (s·a³) = 0`:
  31  differentiating Euler and applying Gibbs–Duhem gives `T·s′ = ρ′`;
  32  continuity then gives `T·(a·s′ + 3a′·s) = 0`, and `T ≠ 0` cancels.
  33  Comoving entropy conservation is a *theorem*, not a postulate.
  34
  35* **§2 (`radiation_aT_conserved`).** For a decoupled radiation gas
  36  (`ρ = αT⁴`, `p = ρ/3`) the continuity equation alone forces
  37  `d/dt (a·T) = 0`: the free-streaming redshift law is a *theorem*.
  38  The equilibrium identities are automatic for radiation
  39  (`radiation_euler`, `radiation_gibbs_duhem`), so no extra physics enters.
  40
  41* **§3 (global constancy).** Pointwise vanishing derivatives upgrade to
  42  `s(t₁)a(t₁)³ = s(t₂)a(t₂)³` and `a(t₁)T(t₁) = a(t₂)T(t₂)` via the mean
  43  value theorem (`is_const_of_deriv_eq_zero`).
  44
  45* **§4 (capstones).** Feeding these into
  46  `NeutrinoDilution.dilution_from_entropy_conservation`:
  47  `(T_ν/T_γ)³ = 4/11` and the present-day entropy `(2π²/45)·(43/11)·T_γ³`
  48  now follow from the continuity equations plus equilibrium thermodynamics —
  49  the former MODEL hypotheses are gone from the chain.
  50
  51## What remains MODEL upstream
  52
  53The Friedmann equations (the GR input), local equilibrium of the coupled
  54sector (Euler + Gibbs–Duhem as named identities), sector decoupling (the
  55neutrino gas satisfies its own continuity equation — no energy exchange),
  56the boundary identifications (plasma dof before/after annihilation, shared
  57temperature at decoupling), and instantaneous decoupling.  All the
  58*dynamics* — that expansion is adiabatic and that free radiation redshifts
  59as `1/a` — is now derived.
  60
  61Reference: Kolb & Turner, *The Early Universe*, §3.3–3.4; Weinberg,
  62*Cosmology*, §1.1 (Bianchi identity and the continuity equation).
  63-/
  64
  65namespace IndisputableMonolith
  66namespace Cosmology
  67namespace EntropyConservationFRW
  68
  69open Real
  70
  71/-! ## §0. The continuity equation from the Friedmann equations -/
  72
  73/-- **THEOREM (continuity from Friedmann).** The FRW continuity equation
  74`a·ρ′ = −3a′(ρ+p)` follows from the two Friedmann equations
  75
  76* I:  `a′² = (8πG/3)·ρ·a²`  (holding along the evolution), and
  77* II: `a″·a = −(4πG/3)·(ρ+3p)·a²`  (at the given time),
  78
  79by differentiating I and eliminating `a″` with II.  No division is used;
  80`G ≠ 0` and `a(t) ≠ 0` cancel the common factor `(8πG/3)·a²`. -/
  81theorem continuity_from_friedmann
  82    {a ρ p : ℝ → ℝ} {a' : ℝ → ℝ} {a'' ρ' G t : ℝ}
  83    (hG : G ≠ 0) (hat : a t ≠ 0)
  84    (had : ∀ u, HasDerivAt a (a' u) u)
  85    (ha'd : HasDerivAt a' a'' t)
  86    (hρd : HasDerivAt ρ ρ' t)
  87    (hF1 : ∀ u, a' u ^ 2 = 8 * π * G / 3 * (ρ u * a u ^ 2))
  88    (hF2 : a'' * a t = -(4 * π * G / 3) * ((ρ t + 3 * p t) * a t ^ 2)) :
  89    a t * ρ' = -3 * a' t * (ρ t + p t) := by
  90  -- Differentiate the first Friedmann equation.
  91  have hL : HasDerivAt (fun u => a' u ^ 2) (2 * a' t * a'') t := by
  92    simpa using ha'd.fun_pow 2
  93  have hpow : HasDerivAt (fun u => a u ^ 2) (2 * a t * a' t) t := by
  94    simpa using (had t).fun_pow 2
  95  have hprod : HasDerivAt (fun u => ρ u * a u ^ 2)
  96      (ρ' * a t ^ 2 + ρ t * (2 * a t * a' t)) t := hρd.mul hpow
  97  have hR : HasDerivAt (fun u => 8 * π * G / 3 * (ρ u * a u ^ 2))
  98      (8 * π * G / 3 * (ρ' * a t ^ 2 + ρ t * (2 * a t * a' t))) t :=
  99    hprod.const_mul (8 * π * G / 3)
 100  have hfun : (fun u => a' u ^ 2)
 101      = fun u => 8 * π * G / 3 * (ρ u * a u ^ 2) := funext hF1
 102  rw [hfun] at hL
 103  have heq : 2 * a' t * a''
 104      = 8 * π * G / 3 * (ρ' * a t ^ 2 + ρ t * (2 * a t * a' t)) :=
 105    hL.unique hR
 106  -- Eliminate a″ with the second Friedmann equation; cancel (8πG/3)·a².
 107  have hπ : (π : ℝ) ≠ 0 := Real.pi_ne_zero
 108  have hC : (8 * π * G / 3 : ℝ) ≠ 0 := by
 109    apply div_ne_zero _ (by norm_num : (3 : ℝ) ≠ 0)
 110    exact mul_ne_zero (mul_ne_zero (by norm_num) hπ) hG
 111  have hkey : 8 * π * G / 3 * a t ^ 2
 112      * (a t * ρ' + 3 * a' t * (ρ t + p t)) = 0 := by
 113    linear_combination 2 * a' t * hF2 - a t * heq
 114  have hcancel :=
 115    (mul_eq_zero.mp hkey).resolve_left (mul_ne_zero hC (pow_ne_zero 2 hat))
 116  linarith
 117
 118/-! ## §1. Comoving entropy conservation for an equilibrium fluid -/
 119
 120/-- **THEOREM (adiabatic expansion derived).** For a fluid in local
 121equilibrium — Euler relation `T·s = ρ + p` along the evolution and
 122Gibbs–Duhem `p′ = s·T′` at the given time — the FRW continuity equation
 123`a·ρ′ = −3a′(ρ+p)` forces `d/dt (s·a³) = 0`.
 124
 125Differentiating the Euler relation gives `T′s + Ts′ = ρ′ + p′`; Gibbs–Duhem
 126removes the `T′` terms, leaving `T·s′ = ρ′`; continuity plus Euler then give
 127`T·(a·s′ + 3a′·s) = 0`, and `T ≠ 0` cancels. -/
 128theorem comoving_entropy_conserved
 129    {ρ p s T a : ℝ → ℝ} {ρ' p' s' a' T' t : ℝ}
 130    (hTt : T t ≠ 0)
 131    (hρ : HasDerivAt ρ ρ' t) (hp : HasDerivAt p p' t)
 132    (hs : HasDerivAt s s' t) (ha : HasDerivAt a a' t)
 133    (hT : HasDerivAt T T' t)
 134    (hEuler : ∀ u, T u * s u = ρ u + p u)
 135    (hGD : p' = s t * T')
 136    (hcont : a t * ρ' = -3 * a' * (ρ t + p t)) :
 137    HasDerivAt (fun u => s u * a u ^ 3) 0 t := by
 138  -- Differentiate the Euler relation.
 139  have hTs : HasDerivAt (fun u => T u * s u) (T' * s t + T t * s') t :=
 140    hT.mul hs
 141  have hρp : HasDerivAt (fun u => ρ u + p u) (ρ' + p') t := hρ.add hp
 142  have hfun : (fun u => T u * s u) = fun u => ρ u + p u := funext hEuler
 143  rw [hfun] at hTs
 144  have hdiff : T' * s t + T t * s' = ρ' + p' := hTs.unique hρp
 145  -- Gibbs–Duhem kills the T′ terms: T·s′ = ρ′.
 146  have hTs' : T t * s' = ρ' := by linear_combination hdiff + hGD
 147  -- Continuity + Euler force a·s′ + 3a′·s = 0.
 148  have hkey : a t * s' + 3 * a' * s t = 0 := by
 149    have h1 : T t * (a t * s' + 3 * a' * s t) = 0 := by
 150      linear_combination a t * hTs' + 3 * a' * hEuler t + hcont
 151    exact (mul_eq_zero.mp h1).resolve_left hTt
 152  -- Assemble the product derivative of s·a³.
 153  have hpow : HasDerivAt (fun u => a u ^ 3) (3 * a t ^ 2 * a') t := by
 154    simpa using ha.fun_pow 3
 155  have hprod : HasDerivAt (fun u => s u * a u ^ 3)
 156      (s' * a t ^ 3 + s t * (3 * a t ^ 2 * a')) t := hs.mul hpow
 157  have hzero : s' * a t ^ 3 + s t * (3 * a t ^ 2 * a') = 0 := by
 158    linear_combination a t ^ 2 * hkey
 159  rw [hzero] at hprod
 160  exact hprod
 161
 162/-! ## §2. Free streaming: a·T conserved for a decoupled radiation gas -/
 163
 164/-- **THEOREM (free streaming derived).** For a decoupled radiation gas with
 165`ρ = αT⁴` and `p = ρ/3`, the FRW continuity equation alone forces
 166`d/dt (a·T) = 0`: the redshift law `T ∝ 1/a` is not an assumption.
 167Continuity reads `4αT³·(a·T′ + a′·T) = 0` and `α ≠ 0`, `T ≠ 0` cancel. -/
 168theorem radiation_aT_conserved
 169    {T a : ℝ → ℝ} {T' a' ρ' t α : ℝ}
 170    (hα : α ≠ 0) (hTt : T t ≠ 0)
 171    (hT : HasDerivAt T T' t) (ha : HasDerivAt a a' t)
 172    (hρ : HasDerivAt (fun u => α * T u ^ 4) ρ' t)
 173    (hcont : a t * ρ' = -3 * a' * (α * T t ^ 4 + α * T t ^ 4 / 3)) :
 174    HasDerivAt (fun u => a u * T u) 0 t := by
 175  -- The density derivative is 4αT³T′ by uniqueness.
 176  have hpow : HasDerivAt (fun u => T u ^ 4) (4 * T t ^ 3 * T') t := by
 177    simpa using hT.fun_pow 4
 178  have h4 : HasDerivAt (fun u => α * T u ^ 4) (α * (4 * T t ^ 3 * T')) t :=
 179    hpow.const_mul α
 180  have hρval : ρ' = α * (4 * T t ^ 3 * T') := hρ.unique h4
 181  -- Continuity collapses to 4αT³·(a′T + aT′) = 0.
 182  have hkey : a' * T t + a t * T' = 0 := by
 183    have h1 : 4 * α * T t ^ 3 * (a' * T t + a t * T') = 0 := by
 184      rw [hρval] at hcont
 185      linear_combination hcont
 186    have hne : (4 * α * T t ^ 3 : ℝ) ≠ 0 :=
 187      mul_ne_zero (mul_ne_zero (by norm_num) hα) (pow_ne_zero 3 hTt)
 188    exact (mul_eq_zero.mp h1).resolve_left hne
 189  have hprod : HasDerivAt (fun u => a u * T u) (a' * T t + a t * T') t :=
 190    ha.mul hT
 191  rw [hkey] at hprod
 192  exact hprod
 193
 194/-- For radiation (`ρ = αT⁴`, `p = ρ/3`, `s = (4/3)αT³`) the Euler relation
 195`T·s = ρ + p` is an algebraic identity — no extra equilibrium input. -/
 196theorem radiation_euler (α T : ℝ) :
 197    T * (4 / 3 * α * T ^ 3) = α * T ^ 4 + α * T ^ 4 / 3 := by ring
 198
 199/-- For radiation the Gibbs–Duhem relation `p′ = s·T′` is automatic:
 200`d/dt (αT⁴/3) = (4/3)αT³·T′`. -/
 201theorem radiation_gibbs_duhem {T : ℝ → ℝ} {T' t α : ℝ}
 202    (hT : HasDerivAt T T' t) :
 203    HasDerivAt (fun u => α * T u ^ 4 / 3) (4 / 3 * α * T t ^ 3 * T') t := by
 204  have hpow : HasDerivAt (fun u => T u ^ 4) (4 * T t ^ 3 * T') t := by
 205    simpa using hT.fun_pow 4
 206  have h := (hpow.const_mul α).div_const 3
 207  have hval : α * (4 * T t ^ 3 * T') / 3 = 4 / 3 * α * T t ^ 3 * T' := by
 208    ring
 209  rw [hval] at h
 210  exact h
 211
 212/-- Composition check: Friedmann I + II plus the equilibrium identities give
 213comoving entropy conservation directly (continuity is not assumed). -/
 214theorem entropy_conserved_from_friedmann
 215    {ρ p s T a : ℝ → ℝ} {a' : ℝ → ℝ} {ρ' p' s' T' a'' G t : ℝ}
 216    (hG : G ≠ 0) (hat : a t ≠ 0) (hTt : T t ≠ 0)
 217    (had : ∀ u, HasDerivAt a (a' u) u)
 218    (ha'd : HasDerivAt a' a'' t)
 219    (hρd : HasDerivAt ρ ρ' t) (hpd : HasDerivAt p p' t)
 220    (hsd : HasDerivAt s s' t) (hTd : HasDerivAt T T' t)
 221    (hF1 : ∀ u, a' u ^ 2 = 8 * π * G / 3 * (ρ u * a u ^ 2))
 222    (hF2 : a'' * a t = -(4 * π * G / 3) * ((ρ t + 3 * p t) * a t ^ 2))
 223    (hEuler : ∀ u, T u * s u = ρ u + p u)
 224    (hGD : p' = s t * T') :
 225    HasDerivAt (fun u => s u * a u ^ 3) 0 t :=
 226  comoving_entropy_conserved hTt hρd hpd hsd (had t) hTd hEuler hGD
 227    (continuity_from_friedmann hG hat had ha'd hρd hF1 hF2)
 228
 229/-! ## §3. Global constancy from pointwise conservation -/
 230
 231/-- **Global adiabaticity.** If the equilibrium fluid satisfies the
 232continuity equation at every time, comoving entropy is the same at any two
 233times: `s(t₁)·a(t₁)³ = s(t₂)·a(t₂)³`. -/
 234theorem comoving_entropy_constant
 235    {ρ p s T a : ℝ → ℝ} {ρ' p' s' a' T' : ℝ → ℝ}
 236    (hTt : ∀ t, T t ≠ 0)
 237    (hρ : ∀ t, HasDerivAt ρ (ρ' t) t) (hp : ∀ t, HasDerivAt p (p' t) t)
 238    (hs : ∀ t, HasDerivAt s (s' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
 239    (hT : ∀ t, HasDerivAt T (T' t) t)
 240    (hEuler : ∀ u, T u * s u = ρ u + p u)
 241    (hGD : ∀ t, p' t = s t * T' t)
 242    (hcont : ∀ t, a t * ρ' t = -3 * a' t * (ρ t + p t))
 243    (t₁ t₂ : ℝ) :
 244    s t₁ * a t₁ ^ 3 = s t₂ * a t₂ ^ 3 := by
 245  have h0 : ∀ t, HasDerivAt (fun u => s u * a u ^ 3) 0 t := fun t =>
 246    comoving_entropy_conserved (hTt t) (hρ t) (hp t) (hs t) (ha t) (hT t)
 247      hEuler (hGD t) (hcont t)
 248  exact is_const_of_deriv_eq_zero (fun t => (h0 t).differentiableAt)
 249    (fun t => (h0 t).deriv) t₁ t₂
 250
 251/-- **Global free streaming.** If the decoupled radiation gas satisfies its
 252continuity equation at every time, `a·T` is the same at any two times. -/
 253theorem radiation_aT_constant
 254    {T a : ℝ → ℝ} {T' a' ρ' : ℝ → ℝ} {α : ℝ}
 255    (hα : α ≠ 0) (hTt : ∀ t, T t ≠ 0)
 256    (hT : ∀ t, HasDerivAt T (T' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
 257    (hρ : ∀ t, HasDerivAt (fun u => α * T u ^ 4) (ρ' t) t)
 258    (hcont : ∀ t, a t * ρ' t
 259        = -3 * a' t * (α * T t ^ 4 + α * T t ^ 4 / 3))
 260    (t₁ t₂ : ℝ) :
 261    a t₁ * T t₁ = a t₂ * T t₂ := by
 262  have h0 : ∀ t, HasDerivAt (fun u => a u * T u) 0 t := fun t =>
 263    radiation_aT_conserved hα (hTt t) (hT t) (ha t) (hρ t) (hcont t)
 264  exact is_const_of_deriv_eq_zero (fun t => (h0 t).differentiableAt)
 265    (fun t => (h0 t).deriv) t₁ t₂
 266
 267/-! ## §4. Capstones: the dilution and g*s from the continuity equations -/
 268
 269/-- **CAPSTONE (dilution from FRW dynamics).** Replace the two MODEL
 270hypotheses of `NeutrinoDilution.dilution_from_entropy_conservation` by
 271physics: the coupled sector is an equilibrium fluid (Euler + Gibbs–Duhem)
 272satisfying the FRW continuity equation, and the decoupled neutrino gas is
 273free radiation (`ρ_ν = α_ν T_ν⁴`) satisfying its own continuity equation.
 274Then comoving entropy conservation and the `1/a` redshift law are *derived*
 275(§§1–3), and with the boundary data (plasma dof `2+4 → 2` across e±
 276annihilation, shared temperature at decoupling) they force
 277
 278  `(T_ν/T_γ)³ = 4/11`. -/
 279theorem dilution_from_frw
 280    {ρ p s T a Tν : ℝ → ℝ} {ρ' p' s' a' T' Tν' ρν' : ℝ → ℝ}
 281    {t₁ t₂ : ℝ} {T₁ Tγ αν : ℝ}
 282    (hTt : ∀ t, T t ≠ 0) (hαν : αν ≠ 0) (hTνt : ∀ t, Tν t ≠ 0)
 283    (ha₂ : a t₂ ≠ 0) (hTγ : Tγ ≠ 0)
 284    (hρ : ∀ t, HasDerivAt ρ (ρ' t) t) (hp : ∀ t, HasDerivAt p (p' t) t)
 285    (hs : ∀ t, HasDerivAt s (s' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
 286    (hT : ∀ t, HasDerivAt T (T' t) t)
 287    (hTν : ∀ t, HasDerivAt Tν (Tν' t) t)
 288    (hρν : ∀ t, HasDerivAt (fun u => αν * Tν u ^ 4) (ρν' t) t)
 289    (hEuler : ∀ u, T u * s u = ρ u + p u)
 290    (hGD : ∀ t, p' t = s t * T' t)
 291    (hcont : ∀ t, a t * ρ' t = -3 * a' t * (ρ t + p t))
 292    (hcontν : ∀ t, a t * ρν' t
 293        = -3 * a' t * (αν * Tν t ^ 4 + αν * Tν t ^ 4 / 3))
 294    (hbefore : s t₁ = NeutrinoDilution.radiationEntropy 2 4 T₁)
 295    (hafter : s t₂ = NeutrinoDilution.radiationEntropy 2 0 Tγ)
 296    (hshare : Tν t₁ = T₁) :
 297    (Tν t₂ / Tγ) ^ 3 = 4 / 11 := by
 298  -- Adiabaticity of the coupled sector (derived, §§1, 3).
 299  have hcons : NeutrinoDilution.radiationEntropy 2 4 T₁ * a t₁ ^ 3
 300      = NeutrinoDilution.radiationEntropy 2 0 Tγ * a t₂ ^ 3 := by
 301    have h := comoving_entropy_constant hTt hρ hp hs ha hT hEuler hGD hcont t₁ t₂
 302    rw [hbefore, hafter] at h
 303    exact h
 304  -- Free streaming of the neutrino sector (derived, §§2, 3).
 305  have hfree : a t₂ * Tν t₂ = a t₁ * T₁ := by
 306    have h := radiation_aT_constant hαν hTνt hTν ha hρν hcontν t₂ t₁
 307    rw [hshare] at h
 308    exact h
 309  exact NeutrinoDilution.dilution_from_entropy_conservation ha₂ hTγ hcons hfree
 310
 311/-- **CAPSTONE (g*s from FRW dynamics).** With the same physics inputs, the
 312present-day entropy density (photons at `T_γ` + 6 fermionic neutrino dof at
 313the diluted `T_ν`) equals `(2π²/45)·gStarS·T_γ³` with
 314`EntropyPerPhoton.gStarS = 43/11`: the effective entropy dof entering the
 315η_B dynamical prefactor is forced by the continuity equations. -/
 316theorem gStarS_from_frw
 317    {ρ p s T a Tν : ℝ → ℝ} {ρ' p' s' a' T' Tν' ρν' : ℝ → ℝ}
 318    {t₁ t₂ : ℝ} {T₁ Tγ αν : ℝ}
 319    (hTt : ∀ t, T t ≠ 0) (hαν : αν ≠ 0) (hTνt : ∀ t, Tν t ≠ 0)
 320    (ha₂ : a t₂ ≠ 0) (hTγ : Tγ ≠ 0)
 321    (hρ : ∀ t, HasDerivAt ρ (ρ' t) t) (hp : ∀ t, HasDerivAt p (p' t) t)
 322    (hs : ∀ t, HasDerivAt s (s' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
 323    (hT : ∀ t, HasDerivAt T (T' t) t)
 324    (hTν : ∀ t, HasDerivAt Tν (Tν' t) t)
 325    (hρν : ∀ t, HasDerivAt (fun u => αν * Tν u ^ 4) (ρν' t) t)
 326    (hEuler : ∀ u, T u * s u = ρ u + p u)
 327    (hGD : ∀ t, p' t = s t * T' t)
 328    (hcont : ∀ t, a t * ρ' t = -3 * a' t * (ρ t + p t))
 329    (hcontν : ∀ t, a t * ρν' t
 330        = -3 * a' t * (αν * Tν t ^ 4 + αν * Tν t ^ 4 / 3))
 331    (hbefore : s t₁ = NeutrinoDilution.radiationEntropy 2 4 T₁)
 332    (hafter : s t₂ = NeutrinoDilution.radiationEntropy 2 0 Tγ)
 333    (hshare : Tν t₁ = T₁) :
 334    NeutrinoDilution.radiationEntropy 2 0 Tγ
 335        + NeutrinoDilution.radiationEntropy 0 6 (Tν t₂)
 336      = 2 * π ^ 2 / 45 * ((EntropyPerPhoton.gStarS : ℚ) : ℝ) * Tγ ^ 3 :=
 337  NeutrinoDilution.total_entropy_eq_gStarS hTγ
 338    (dilution_from_frw hTt hαν hTνt ha₂ hTγ hρ hp hs ha hT hTν hρν
 339      hEuler hGD hcont hcontν hbefore hafter hshare)
 340
 341end EntropyConservationFRW
 342end Cosmology
 343end IndisputableMonolith
 344