Encyclopedia Cosmology Cosmology Entropy Conservation Frw Entropy Conserved From Friedmann

ARTICLE 4 claims 4 theorems

Cosmology Entropy Conservation Frw Entropy Conserved From Friedmann

In an expanding universe, the total entropy in a patch of space stays constant; a machine-checked proof shows this follows from Einstein's equations, not from an extra assumption.

Verify this page

Why entropy stays put

In cosmology, a central quantity is the entropy inside a volume that expands with the universe. As space grows, the entropy density drops, but the total entropy in that comoving volume is expected to stay fixed. This conservation is what lets cosmologists track how the early universe cooled and how particle populations changed. The standard story treats this as an assumption, but a machine-checked library of formal theorems shows it can be derived from more basic physics.

The derivation starts with the Friedmann equations, which describe how the scale factor a (the universe's size) evolves. From these two equations, the library proves the continuity equation: a·ρ′ = −3a′(ρ+p), where ρ is energy density and p is pressure. This is not new physics; it is the Bianchi identity, a consistency condition that any solution to Einstein's equations must satisfy. The library proves it formally, without dividing by any quantity that could be zero.

Next, the library takes a fluid in local equilibrium, meaning its temperature, entropy density, pressure, and energy density are linked by the Euler relation T·s = ρ + p and the Gibbs–Duhem relation p′ = s·T′. Combining these with the continuity equation forces the derivative of s·a³ to be zero. In plain words, the entropy in a comoving volume is constant. The theorem entropy_conserved_from_friedmann packages this result: given the two Friedmann equations and the equilibrium relations, it proves the entropy conservation directly, with no separate postulate.

The same machinery derives the redshift law for radiation. For a decoupled gas of photons or neutrinos, with energy density proportional to T⁴, the continuity equation alone forces a·T to be constant. This means the temperature drops as 1/a, the familiar cooling of the universe, now proved rather than assumed. From these two results, the library derives the standard neutrino dilution factor: the ratio of neutrino to photon temperature cubed equals 4/11, and the effective number of entropy degrees of freedom is 43/11.

What remains as input is not the dynamics but the setup. The Friedmann equations themselves are taken from general relativity. The library assumes the fluid is in local equilibrium, that the neutrino gas is decoupled and satisfies its own continuity equation, and that the particle content changes at electron-positron annihilation. These are physical models, not derived facts. The theorem does not claim to explain why the universe is adiabatic; it shows that adiabaticity follows from the equations of motion plus equilibrium thermodynamics.

THEOREM continuity_from_friedmann · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean
continuity_from_friedmann · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean:73 
/-- **THEOREM (continuity from Friedmann).** The FRW continuity equation
`a·ρ′ = −3a′(ρ+p)` follows from the two Friedmann equations

* I:  `a′² = (8πG/3)·ρ·a²`  (holding along the evolution), and
* II: `a″·a = −(4πG/3)·(ρ+3p)·a²`  (at the given time),

by differentiating I and eliminating `a″` with II.  No division is used;
`G ≠ 0` and `a(t) ≠ 0` cancel the common factor `(8πG/3)·a²`. -/
theorem continuity_from_friedmann
    {a ρ p : ℝ → ℝ} {a' : ℝ → ℝ} {a'' ρ' G t : ℝ}
    (hG : G ≠ 0) (hat : a t ≠ 0)
    (had : ∀ u, HasDerivAt a (a' u) u)
    (ha'd : HasDerivAt a' a'' t)
    (hρd : HasDerivAt ρ ρ' t)
    (hF1 : ∀ u, a' u ^ 2 = 8 * π * G / 3 * (ρ u * a u ^ 2))
    (hF2 : a'' * a t = -(4 * π * G / 3) * ((ρ t + 3 * p t) * a t ^ 2)) :
    a t * ρ' = -3 * a' t * (ρ t + p t) := by
  -- Differentiate the first Friedmann equation.
  have hL : HasDerivAt (fun u => a' u ^ 2) (2 * a' t * a'') t := by
    simpa using ha'd.fun_pow 2
  have hpow : HasDerivAt (fun u => a u ^ 2) (2 * a t * a' t) t := by
    simpa using (had t).fun_pow 2
  have hprod : HasDerivAt (fun u => ρ u * a u ^ 2)
      (ρ' * a t ^ 2 + ρ t * (2 * a t * a' t)) t := hρd.mul hpow
  have hR : HasDerivAt (fun u => 8 * π * G / 3 * (ρ u * a u ^ 2))
      (8 * π * G / 3 * (ρ' * a t ^ 2 + ρ t * (2 * a t * a' t))) t :=
    hprod.const_mul (8 * π * G / 3)
  have hfun : (fun u => a' u ^ 2)
      = fun u => 8 * π * G / 3 * (ρ u * a u ^ 2) := funext hF1
  rw [hfun] at hL
  have heq : 2 * a' t * a''
      = 8 * π * G / 3 * (ρ' * a t ^ 2 + ρ t * (2 * a t * a' t)) :=
    hL.unique hR
  -- Eliminate a″ with the second Friedmann equation; cancel (8πG/3)·a².
  have hπ : (π : ℝ) ≠ 0 := Real.pi_ne_zero
  have hC : (8 * π * G / 3 : ℝ) ≠ 0 := by
    apply div_ne_zero _ (by norm_num : (3 : ℝ) ≠ 0)
    exact mul_ne_zero (mul_ne_zero (by norm_num) hπ) hG
  have hkey : 8 * π * G / 3 * a t ^ 2
      * (a t * ρ' + 3 * a' t * (ρ t + p t)) = 0 := by
    linear_combination 2 * a' t * hF2 - a t * heq
  have hcancel :=
    (mul_eq_zero.mp hkey).resolve_left (mul_ne_zero hC (pow_ne_zero 2 hat))
  linarith
THEOREM comoving_entropy_conserved · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean
comoving_entropy_conserved · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean:120 
/-- **THEOREM (adiabatic expansion derived).** For a fluid in local
equilibrium — Euler relation `T·s = ρ + p` along the evolution and
Gibbs–Duhem `p′ = s·T′` at the given time — the FRW continuity equation
`a·ρ′ = −3a′(ρ+p)` forces `d/dt (s·a³) = 0`.

Differentiating the Euler relation gives `T′s + Ts′ = ρ′ + p′`; Gibbs–Duhem
removes the `T′` terms, leaving `T·s′ = ρ′`; continuity plus Euler then give
`T·(a·s′ + 3a′·s) = 0`, and `T ≠ 0` cancels. -/
theorem comoving_entropy_conserved
    {ρ p s T a : ℝ → ℝ} {ρ' p' s' a' T' t : ℝ}
    (hTt : T t ≠ 0)
    (hρ : HasDerivAt ρ ρ' t) (hp : HasDerivAt p p' t)
    (hs : HasDerivAt s s' t) (ha : HasDerivAt a a' t)
    (hT : HasDerivAt T T' t)
    (hEuler : ∀ u, T u * s u = ρ u + p u)
    (hGD : p' = s t * T')
    (hcont : a t * ρ' = -3 * a' * (ρ t + p t)) :
    HasDerivAt (fun u => s u * a u ^ 3) 0 t := by
  -- Differentiate the Euler relation.
  have hTs : HasDerivAt (fun u => T u * s u) (T' * s t + T t * s') t :=
    hT.mul hs
  have hρp : HasDerivAt (fun u => ρ u + p u) (ρ' + p') t := hρ.add hp
  have hfun : (fun u => T u * s u) = fun u => ρ u + p u := funext hEuler
  rw [hfun] at hTs
  have hdiff : T' * s t + T t * s' = ρ' + p' := hTs.unique hρp
  -- Gibbs–Duhem kills the T′ terms: T·s′ = ρ′.
  have hTs' : T t * s' = ρ' := by linear_combination hdiff + hGD
  -- Continuity + Euler force a·s′ + 3a′·s = 0.
  have hkey : a t * s' + 3 * a' * s t = 0 := by
    have h1 : T t * (a t * s' + 3 * a' * s t) = 0 := by
      linear_combination a t * hTs' + 3 * a' * hEuler t + hcont
    exact (mul_eq_zero.mp h1).resolve_left hTt
  -- Assemble the product derivative of s·a³.
  have hpow : HasDerivAt (fun u => a u ^ 3) (3 * a t ^ 2 * a') t := by
    simpa using ha.fun_pow 3
  have hprod : HasDerivAt (fun u => s u * a u ^ 3)
      (s' * a t ^ 3 + s t * (3 * a t ^ 2 * a')) t := hs.mul hpow
  have hzero : s' * a t ^ 3 + s t * (3 * a t ^ 2 * a') = 0 := by
    linear_combination a t ^ 2 * hkey
  rw [hzero] at hprod
  exact hprod
THEOREM radiation_aT_conserved · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean
radiation_aT_conserved · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean:164 
/-- **THEOREM (free streaming derived).** For a decoupled radiation gas with
`ρ = αT⁴` and `p = ρ/3`, the FRW continuity equation alone forces
`d/dt (a·T) = 0`: the redshift law `T ∝ 1/a` is not an assumption.
Continuity reads `4αT³·(a·T′ + a′·T) = 0` and `α ≠ 0`, `T ≠ 0` cancel. -/
theorem radiation_aT_conserved
    {T a : ℝ → ℝ} {T' a' ρ' t α : ℝ}
    (hα : α ≠ 0) (hTt : T t ≠ 0)
    (hT : HasDerivAt T T' t) (ha : HasDerivAt a a' t)
    (hρ : HasDerivAt (fun u => α * T u ^ 4) ρ' t)
    (hcont : a t * ρ' = -3 * a' * (α * T t ^ 4 + α * T t ^ 4 / 3)) :
    HasDerivAt (fun u => a u * T u) 0 t := by
  -- The density derivative is 4αT³T′ by uniqueness.
  have hpow : HasDerivAt (fun u => T u ^ 4) (4 * T t ^ 3 * T') t := by
    simpa using hT.fun_pow 4
  have h4 : HasDerivAt (fun u => α * T u ^ 4) (α * (4 * T t ^ 3 * T')) t :=
    hpow.const_mul α
  have hρval : ρ' = α * (4 * T t ^ 3 * T') := hρ.unique h4
  -- Continuity collapses to 4αT³·(a′T + aT′) = 0.
  have hkey : a' * T t + a t * T' = 0 := by
    have h1 : 4 * α * T t ^ 3 * (a' * T t + a t * T') = 0 := by
      rw [hρval] at hcont
      linear_combination hcont
    have hne : (4 * α * T t ^ 3 : ℝ) ≠ 0 :=
      mul_ne_zero (mul_ne_zero (by norm_num) hα) (pow_ne_zero 3 hTt)
    exact (mul_eq_zero.mp h1).resolve_left hne
  have hprod : HasDerivAt (fun u => a u * T u) (a' * T t + a t * T') t :=
    ha.mul hT
  rw [hkey] at hprod
  exact hprod
THEOREM entropy_conserved_from_friedmann · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean
entropy_conserved_from_friedmann · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean:212 
/-- Composition check: Friedmann I + II plus the equilibrium identities give
comoving entropy conservation directly (continuity is not assumed). -/
theorem entropy_conserved_from_friedmann
    {ρ p s T a : ℝ → ℝ} {a' : ℝ → ℝ} {ρ' p' s' T' a'' G t : ℝ}
    (hG : G ≠ 0) (hat : a t ≠ 0) (hTt : T t ≠ 0)
    (had : ∀ u, HasDerivAt a (a' u) u)
    (ha'd : HasDerivAt a' a'' t)
    (hρd : HasDerivAt ρ ρ' t) (hpd : HasDerivAt p p' t)
    (hsd : HasDerivAt s s' t) (hTd : HasDerivAt T T' t)
    (hF1 : ∀ u, a' u ^ 2 = 8 * π * G / 3 * (ρ u * a u ^ 2))
    (hF2 : a'' * a t = -(4 * π * G / 3) * ((ρ t + 3 * p t) * a t ^ 2))
    (hEuler : ∀ u, T u * s u = ρ u + p u)
    (hGD : p' = s t * T') :
    HasDerivAt (fun u => s u * a u ^ 3) 0 t :=
  comoving_entropy_conserved hTt hρd hpd hsd (had t) hTd hEuler hGD
    (continuity_from_friedmann hG hat had ha'd hρd hF1 hF2)

What this page does not claim

The Friedmann equations themselves are not derived; they are the general relativity input. The theorem does not prove that the universe is adiabatic; it proves adiabaticity follows from the equations plus equilibrium thermodynamics. The theorem does not derive the particle content or the decoupling temperature; those are boundary data.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/EntropyConservationFRW.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND