IndisputableMonolith.Cosmology.GrandPotential
IndisputableMonolith/Cosmology/GrandPotential.lean · 342 lines · 17 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cosmology.RadiationEntropyRelation
3import IndisputableMonolith.Cosmology.FermionWeightIntegral
4import IndisputableMonolith.Cosmology.EntropyConservationFRW
5
6/-!
7# Euler and Gibbs–Duhem from the Grand Potential
8
9**Status: THEOREM (this module, 0 sorry).**
10
11`EntropyConservationFRW` derived comoving entropy conservation from the FRW
12continuity equation *given* two named equilibrium identities:
13
14* Euler relation `T·s = ρ + p`, and
15* Gibbs–Duhem relation `p′ = s·T′`.
16
17This module discharges both. In the grand-canonical ensemble at zero chemical
18potential a fluid is characterised by a single thermodynamic potential — the
19pressure `P(T)` (equivalently the grand potential density `Ω = −P`). Entropy
20density is *defined* as `s = dP/dT` and energy density by the Legendre
21transform `ρ = T·s − P`. With that structure:
22
23* **Euler** `T·s = ρ + P` is an algebraic identity of the Legendre transform
24 (`potential_euler`),
25* **Gibbs–Duhem** `d/dt P(T(t)) = s·T′` is the chain rule
26 (`potential_gibbs_duhem`), and
27* the fundamental relation **`dρ = T·ds`** follows (`energy_deriv`):
28 `ρ′(T) = s + T·s′ − s = T·s′`.
29
30So the two hypotheses of `comoving_entropy_conserved` collapse into ONE
31structural statement — "the coupled sector's pressure is a differentiable
32potential with `s = dP/dT`" — which is the *definition* of local equilibrium,
33not an extra dynamical assumption (`potential_entropy_conserved`).
34
35## The concrete plasma realizes the structure
36
37§2 instantiates the potential with statistical mechanics. The pressure of a
38massless Bose/Fermi gas is the log-kernel integral of the grand partition
39function:
40
41 `P = (g_B/2π²)·T⁴·∫ t²(−ln(1−e^{−t})) dt + (g_F/2π²)·T⁴·∫ t² ln(1+e^{−t}) dt`
42
43The two integrals were **derived** in `RadiationEntropyRelation` via Mellin
44transforms (`π⁴/45` and `7π⁴/360`), giving
45
46 `P = (π²/90)·(g_B + (7/8)·g_F)·T⁴` (`plasmaPressure_eq`).
47
48Its temperature derivative is *exactly* the `radiationEntropy` of
49`NeutrinoDilution` (`plasmaPressure_potential`) — the same object previously
50obtained from the independent entropy integrals `∫σ_B = 4π⁴/45`,
51`∫σ_F = 7π⁴/90`. And the Legendre transform `T·s − P` reproduces the
52independently derived energy integrals `π⁴/15`, `7π⁴/120`
53(`plasma_energyOf`), forcing the radiation equation of state `p = ρ/3`
54(`plasma_eos`) — the EOS is a *theorem* of the ensemble, not an input.
55
56## Capstone
57
58`dilution_from_potential`: the neutrino dilution `(T_ν/T_γ)³ = 4/11` now
59follows from: FRW continuity for each sector + "the coupled sector has a
60pressure potential" + boundary data. Euler and Gibbs–Duhem are gone from the
61hypothesis list; `gStarS_from_potential` propagates this to `g*s = 43/11`,
62the effective dof in the η_B dynamical prefactor.
63
64## What remains MODEL upstream
65
66The grand-canonical form of the plasma pressure at the boundaries (statistical
67mechanics input, though its integrals are derived), the Friedmann equations
68behind the continuity equation (discharged separately in
69`EntropyConservationFRW.continuity_from_friedmann`), sector decoupling, and
70the boundary identifications (dof `2+4 → 2` across e± annihilation, shared
71temperature at decoupling).
72
73Reference: Landau & Lifshitz, *Statistical Physics* §24–§27 (grand potential,
74`Ω = −PV`, `S = −∂Ω/∂T`); Kolb & Turner §3.3–3.4.
75-/
76
77namespace IndisputableMonolith
78namespace Cosmology
79namespace GrandPotential
80
81open Real MeasureTheory Set
82
83/-! ## §1. The abstract potential fluid -/
84
85/-- Energy density of a potential fluid: the Legendre transform of the
86pressure potential, `ρ(T) = T·s(T) − P(T)`, with `s = dP/dT`. This is
87`ρ = T·(∂P/∂T) − P`, i.e. `U = TS − PV + μN` per unit volume at `μ = 0`. -/
88noncomputable def energyOf (P s : ℝ → ℝ) : ℝ → ℝ := fun x => x * s x - P x
89
90/-- **Euler relation (derived).** `T·s = ρ + P` is an algebraic identity of
91the Legendre-transform structure — not an independent equilibrium postulate. -/
92theorem potential_euler (P s : ℝ → ℝ) (x : ℝ) :
93 x * s x = energyOf P s x + P x := by
94 simp only [energyOf]
95 ring
96
97/-- **Gibbs–Duhem relation (derived).** Along any temperature trajectory
98`T(t)`, the pressure obeys `p′ = s(T)·T′`: this is the chain rule applied to
99`s = dP/dT`, not an independent postulate. -/
100theorem potential_gibbs_duhem
101 {P s T : ℝ → ℝ} {T' t : ℝ}
102 (hP : HasDerivAt P (s (T t)) (T t))
103 (hT : HasDerivAt T T' t) :
104 HasDerivAt (fun u => P (T u)) (s (T t) * T') t := by
105 simpa [Function.comp] using hP.comp t hT
106
107/-- Entropy along a trajectory: `d/dt s(T(t)) = s′(T)·T′` (chain rule). -/
108theorem potential_entropy_deriv
109 {s T : ℝ → ℝ} {sT T' t : ℝ}
110 (hs : HasDerivAt s sT (T t))
111 (hT : HasDerivAt T T' t) :
112 HasDerivAt (fun u => s (T u)) (sT * T') t := by
113 simpa [Function.comp] using hs.comp t hT
114
115/-- **Fundamental relation `dρ = T·ds` (derived).** The energy density of a
116potential fluid has temperature derivative `ρ′(T) = T·s′(T)`:
117differentiating `ρ = T·s − P` gives `s + T·s′ − s`. -/
118theorem energy_deriv
119 {P s : ℝ → ℝ} {sT x : ℝ}
120 (hP : HasDerivAt P (s x) x)
121 (hs : HasDerivAt s sT x) :
122 HasDerivAt (energyOf P s) (x * sT) x := by
123 have hid : HasDerivAt (fun y : ℝ => y) 1 x := hasDerivAt_id x
124 have hxs : HasDerivAt (fun y => y * s y) (1 * s x + x * sT) x := hid.mul hs
125 have h : HasDerivAt (fun y => y * s y - P y)
126 (1 * s x + x * sT - s x) x := hxs.sub hP
127 have hval : 1 * s x + x * sT - s x = x * sT := by ring
128 rw [hval] at h
129 exact h
130
131/-- Energy along a trajectory: `d/dt ρ(T(t)) = T·s′(T)·T′`. -/
132theorem potential_energy_deriv
133 {P s T : ℝ → ℝ} {sT T' t : ℝ}
134 (hP : HasDerivAt P (s (T t)) (T t))
135 (hs : HasDerivAt s sT (T t))
136 (hT : HasDerivAt T T' t) :
137 HasDerivAt (fun u => energyOf P s (T u)) (T t * sT * T') t := by
138 have hx : HasDerivAt (energyOf P s) (T t * sT) (T t) := energy_deriv hP hs
139 simpa [Function.comp, mul_assoc] using hx.comp t hT
140
141/-- **THEOREM (entropy conservation from the potential alone).** For a fluid
142whose pressure is a differentiable potential with `s = dP/dT` — the definition
143of local equilibrium at zero chemical potential — the FRW continuity equation
144forces `d/dt (s·a³) = 0`. The Euler and Gibbs–Duhem hypotheses of
145`EntropyConservationFRW.comoving_entropy_conserved` are *derived* here
146(`potential_euler`, `potential_gibbs_duhem`), not assumed. -/
147theorem potential_entropy_conserved
148 {P s : ℝ → ℝ} {T a : ℝ → ℝ} {sT T' a' t : ℝ}
149 (hTt : T t ≠ 0)
150 (hP : HasDerivAt P (s (T t)) (T t))
151 (hs : HasDerivAt s sT (T t))
152 (hT : HasDerivAt T T' t) (ha : HasDerivAt a a' t)
153 (hcont : a t * (T t * sT * T')
154 = -3 * a' * (energyOf P s (T t) + P (T t))) :
155 HasDerivAt (fun u => s (T u) * a u ^ 3) 0 t :=
156 EntropyConservationFRW.comoving_entropy_conserved hTt
157 (potential_energy_deriv hP hs hT)
158 (potential_gibbs_duhem hP hT)
159 (potential_entropy_deriv hs hT)
160 ha hT
161 (fun u => potential_euler P s (T u))
162 rfl
163 hcont
164
165/-- **Global adiabaticity from the potential.** If the potential structure and
166the continuity equation hold at every time, comoving entropy is globally
167constant: `s(T(t₁))·a(t₁)³ = s(T(t₂))·a(t₂)³`. -/
168theorem potential_entropy_constant
169 {P s : ℝ → ℝ} {T a : ℝ → ℝ} {sT T' a' : ℝ → ℝ}
170 (hTt : ∀ t, T t ≠ 0)
171 (hP : ∀ t, HasDerivAt P (s (T t)) (T t))
172 (hs : ∀ t, HasDerivAt s (sT t) (T t))
173 (hT : ∀ t, HasDerivAt T (T' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
174 (hcont : ∀ t, a t * (T t * sT t * T' t)
175 = -3 * a' t * (energyOf P s (T t) + P (T t)))
176 (t₁ t₂ : ℝ) :
177 s (T t₁) * a t₁ ^ 3 = s (T t₂) * a t₂ ^ 3 := by
178 have h0 : ∀ t, HasDerivAt (fun u => s (T u) * a u ^ 3) 0 t := fun t =>
179 potential_entropy_conserved (hTt t) (hP t) (hs t) (hT t) (ha t) (hcont t)
180 exact is_const_of_deriv_eq_zero (fun t => (h0 t).differentiableAt)
181 (fun t => (h0 t).deriv) t₁ t₂
182
183/-! ## §2. The relativistic plasma realizes the potential structure -/
184
185/-- Pressure of a massless Bose/Fermi plasma from the grand partition
186function: `P = (g/2π²)·T⁴·∫ t²(−ln(1∓e^{−t})) dt` per sector. The log
187kernels are the grand-canonical `ln Z` integrands after the angular
188integration and the substitution `t = E/T`. -/
189noncomputable def plasmaPressure (gB gF T : ℝ) : ℝ :=
190 gB / (2 * π ^ 2) * T ^ 4
191 * (∫ t in Ioi (0 : ℝ), t ^ 2 * (-Real.log (1 - Real.exp (-t))))
192 + gF / (2 * π ^ 2) * T ^ 4
193 * (∫ t in Ioi (0 : ℝ), t ^ 2 * Real.log (1 + Real.exp (-t)))
194
195/-- Energy density of the same plasma from the occupation-number integrals
196`∫ t³/(eᵗ∓1) dt` (derived in `FermionWeightIntegral`). -/
197noncomputable def plasmaEnergy (gB gF T : ℝ) : ℝ :=
198 gB / (2 * π ^ 2) * T ^ 4
199 * (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1))
200 + gF / (2 * π ^ 2) * T ^ 4
201 * (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t + 1))
202
203/-- **THEOREM (plasma pressure closed form).** The log-kernel integrals
204(`π⁴/45`, `7π⁴/360`, both derived via Mellin transforms) collapse the
205pressure to `P = (π²/90)·(g_B + (7/8)·g_F)·T⁴`. The `7/8` is the same
206fermionic weight that appears in entropy and energy — here it comes out of
207the pressure channel independently. -/
208theorem plasmaPressure_eq (gB gF T : ℝ) :
209 plasmaPressure gB gF T = π ^ 2 / 90 * (gB + 7 / 8 * gF) * T ^ 4 := by
210 unfold plasmaPressure
211 rw [RadiationEntropyRelation.boseLog_integral_value,
212 RadiationEntropyRelation.fermiLog_integral_value]
213 have hπ : (π : ℝ) ≠ 0 := Real.pi_ne_zero
214 field_simp
215 ring
216
217/-- **THEOREM (plasma energy closed form).** The energy integrals (`π⁴/15`,
218`7π⁴/120`) give `ρ = (π²/30)·(g_B + (7/8)·g_F)·T⁴`. -/
219theorem plasmaEnergy_eq (gB gF T : ℝ) :
220 plasmaEnergy gB gF T = π ^ 2 / 30 * (gB + 7 / 8 * gF) * T ^ 4 := by
221 unfold plasmaEnergy
222 rw [FermionWeightIntegral.bose_integral_value,
223 FermionWeightIntegral.fermi_integral_value]
224 have hπ : (π : ℝ) ≠ 0 := Real.pi_ne_zero
225 field_simp
226 ring
227
228/-- **THEOREM (the plasma is a potential fluid).** The temperature derivative
229of the statistical-mechanical pressure is *exactly* the `radiationEntropy` of
230`NeutrinoDilution` — the object previously built from the independent entropy
231integrals `∫σ_B`, `∫σ_F`. So `s = dP/dT` holds between two independently
232derived statistical-mechanical quantities: the potential structure of the
233plasma is a theorem, not a definition. -/
234theorem plasmaPressure_potential (gB gF x : ℝ) :
235 HasDerivAt (fun T => plasmaPressure gB gF T)
236 (NeutrinoDilution.radiationEntropy gB gF x) x := by
237 rw [NeutrinoDilution.radiationEntropy_eq]
238 have hfun : (fun T => plasmaPressure gB gF T)
239 = fun T => π ^ 2 / 90 * (gB + 7 / 8 * gF) * T ^ 4 :=
240 funext fun T => plasmaPressure_eq gB gF T
241 rw [hfun]
242 have hpow : HasDerivAt (fun T : ℝ => T ^ 4) (4 * x ^ 3) x := by
243 simpa using hasDerivAt_pow 4 x
244 have h := hpow.const_mul (π ^ 2 / 90 * (gB + 7 / 8 * gF))
245 have hval : π ^ 2 / 90 * (gB + 7 / 8 * gF) * (4 * x ^ 3)
246 = 2 * π ^ 2 / 45 * (gB + 7 / 8 * gF) * x ^ 3 := by ring
247 rw [hval] at h
248 exact h
249
250/-- **THEOREM (Legendre consistency).** The abstract Legendre energy
251`T·s − P` built from the pressure potential and the entropy equals the
252independently derived energy integral: `∫ t³/(eᵗ∓1)` agrees with
253`4·∫ t²·logkernel − ∫ t²·logkernel`. Two separate ensemble computations
254meet — this is the internal consistency of the grand-canonical structure. -/
255theorem plasma_energyOf (gB gF : ℝ) :
256 energyOf (plasmaPressure gB gF) (NeutrinoDilution.radiationEntropy gB gF)
257 = plasmaEnergy gB gF := by
258 funext T
259 simp only [energyOf]
260 rw [NeutrinoDilution.radiationEntropy_eq, plasmaEnergy_eq, plasmaPressure_eq]
261 ring
262
263/-- **THEOREM (radiation equation of state derived).** `p = ρ/3` is forced by
264the grand-canonical integrals — it is not an input anywhere in the chain. -/
265theorem plasma_eos (gB gF T : ℝ) :
266 plasmaPressure gB gF T = plasmaEnergy gB gF T / 3 := by
267 rw [plasmaEnergy_eq, plasmaPressure_eq]
268 ring
269
270/-! ## §3. Capstones: dilution and g*s with Euler/Gibbs–Duhem discharged -/
271
272/-- **CAPSTONE (dilution from the potential).** `(T_ν/T_γ)³ = 4/11` from:
273the coupled sector has a pressure potential with `s = dP/dT` (local
274equilibrium, the *only* thermodynamic input), both sectors satisfy their FRW
275continuity equations, and the boundary data (plasma dof `2+4 → 2` across e±
276annihilation, shared temperature at decoupling). Compared with
277`EntropyConservationFRW.dilution_from_frw`, the Euler and Gibbs–Duhem
278hypotheses are gone — they are theorems of the potential structure. -/
279theorem dilution_from_potential
280 {P s : ℝ → ℝ} {T a Tν : ℝ → ℝ} {sT T' a' 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 (hP : ∀ t, HasDerivAt P (s (T t)) (T t))
285 (hs : ∀ t, HasDerivAt s (sT t) (T t))
286 (hT : ∀ t, HasDerivAt T (T' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
287 (hTν : ∀ t, HasDerivAt Tν (Tν' t) t)
288 (hρν : ∀ t, HasDerivAt (fun u => αν * Tν u ^ 4) (ρν' t) t)
289 (hcont : ∀ t, a t * (T t * sT t * T' t)
290 = -3 * a' t * (energyOf P s (T t) + P (T t)))
291 (hcontν : ∀ t, a t * ρν' t
292 = -3 * a' t * (αν * Tν t ^ 4 + αν * Tν t ^ 4 / 3))
293 (hbefore : s (T t₁) = NeutrinoDilution.radiationEntropy 2 4 T₁)
294 (hafter : s (T t₂) = NeutrinoDilution.radiationEntropy 2 0 Tγ)
295 (hshare : Tν t₁ = T₁) :
296 (Tν t₂ / Tγ) ^ 3 = 4 / 11 := by
297 -- Adiabaticity of the coupled sector: derived from the potential structure.
298 have hcons : NeutrinoDilution.radiationEntropy 2 4 T₁ * a t₁ ^ 3
299 = NeutrinoDilution.radiationEntropy 2 0 Tγ * a t₂ ^ 3 := by
300 have h := potential_entropy_constant hTt hP hs hT ha hcont t₁ t₂
301 rw [hbefore, hafter] at h
302 exact h
303 -- Free streaming of the neutrino sector (derived in EntropyConservationFRW).
304 have hfree : a t₂ * Tν t₂ = a t₁ * T₁ := by
305 have h := EntropyConservationFRW.radiation_aT_constant hαν hTνt hTν ha
306 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 the potential).** The present-day entropy density
312equals `(2π²/45)·(43/11)·T_γ³` with the same reduced hypothesis list: the
313effective entropy dof in the η_B dynamical prefactor now rests on FRW
314continuity + the existence of a pressure potential + boundary data. -/
315theorem gStarS_from_potential
316 {P s : ℝ → ℝ} {T a Tν : ℝ → ℝ} {sT T' a' Tν' ρν' : ℝ → ℝ}
317 {t₁ t₂ : ℝ} {T₁ Tγ αν : ℝ}
318 (hTt : ∀ t, T t ≠ 0) (hαν : αν ≠ 0) (hTνt : ∀ t, Tν t ≠ 0)
319 (ha₂ : a t₂ ≠ 0) (hTγ : Tγ ≠ 0)
320 (hP : ∀ t, HasDerivAt P (s (T t)) (T t))
321 (hs : ∀ t, HasDerivAt s (sT t) (T t))
322 (hT : ∀ t, HasDerivAt T (T' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
323 (hTν : ∀ t, HasDerivAt Tν (Tν' t) t)
324 (hρν : ∀ t, HasDerivAt (fun u => αν * Tν u ^ 4) (ρν' t) t)
325 (hcont : ∀ t, a t * (T t * sT t * T' t)
326 = -3 * a' t * (energyOf P s (T t) + P (T t)))
327 (hcontν : ∀ t, a t * ρν' t
328 = -3 * a' t * (αν * Tν t ^ 4 + αν * Tν t ^ 4 / 3))
329 (hbefore : s (T t₁) = NeutrinoDilution.radiationEntropy 2 4 T₁)
330 (hafter : s (T t₂) = NeutrinoDilution.radiationEntropy 2 0 Tγ)
331 (hshare : Tν t₁ = T₁) :
332 NeutrinoDilution.radiationEntropy 2 0 Tγ
333 + NeutrinoDilution.radiationEntropy 0 6 (Tν t₂)
334 = 2 * π ^ 2 / 45 * ((EntropyPerPhoton.gStarS : ℚ) : ℝ) * Tγ ^ 3 :=
335 NeutrinoDilution.total_entropy_eq_gStarS hTγ
336 (dilution_from_potential hTt hαν hTνt ha₂ hTγ hP hs hT ha hTν hρν
337 hcont hcontν hbefore hafter hshare)
338
339end GrandPotential
340end Cosmology
341end IndisputableMonolith
342