Encyclopedia Cosmology Cosmology Entropy Conservation Frw Comoving Entropy Conserved

ARTICLE 4 claims 4 theorems

Cosmology Entropy Conservation Frw Comoving Entropy Conserved

In an expanding universe, the entropy inside a comoving volume is conserved: a theorem, not a postulate.

Verify this page

A derived conservation law

In cosmology, a comoving volume is a box that expands with the universe, its edges carried along by the stretching of space. The entropy inside such a box, the number of ways its contents can be arranged at a given temperature, is a quantity of deep interest. Standard cosmology usually assumes this entropy stays constant as the universe expands, an assumption called adiabatic expansion. The Recognition Science framework's machine-checked library of formal theorems proves that this conservation is not an assumption at all: for any fluid in local equilibrium, the Friedmann equations themselves force the comoving entropy to be constant.

The proof chain is short and rigorous. The Friedmann equations, which govern the expansion of the universe, force a continuity equation for the energy density: a·ρ' = −3a'(ρ + p). This is not an independent assumption; it follows from differentiating the first Friedmann equation and eliminating the acceleration using the second. For a fluid in local equilibrium, where the Euler relation T·s = ρ + p and the Gibbs–Duhem relation p' = s·T' hold, this continuity equation forces the derivative of s·a³ to vanish. The calculation is direct: differentiating the Euler relation and applying Gibbs–Duhem leaves T·s' = ρ', and substituting the continuity equation gives T·(a·s' + 3a'·s) = 0. Since the temperature T is nonzero, the term in parentheses must be zero, which is exactly the statement that s·a³ has zero time derivative.

This pointwise result upgrades to a global statement. If the fluid satisfies the continuity equation at every time, then the comoving entropy at any two times is equal: s(t₁)·a(t₁)³ = s(t₂)·a(t₂)³. The same derivation applies to a decoupled radiation gas, where it forces the free-streaming redshift law a·T = constant, meaning the temperature of freely streaming radiation falls as 1/a. Both results feed into the framework's capstone theorems, which derive the neutrino dilution ratio (T_ν/T_γ)³ = 4/11 and the effective entropy degrees of freedom g*s = 43/11 from the continuity equations plus equilibrium thermodynamics, without assuming adiabatic expansion or free streaming as separate postulates.

What the declaration does not claim is just as important as what it proves. The Friedmann equations themselves, the local equilibrium of the coupled sector, the decoupling of the neutrino gas, and the boundary identifications across electron-positron annihilation all remain model inputs. The theorem proves the dynamics of expansion are adiabatic, but it does not prove the universe is adiabatic; it proves free radiation redshifts as 1/a, but it does not prove the neutrino gas is free. Those are physical assumptions about the early universe, not consequences of the mathematics.

THEOREM comoving_entropy_conserved · entropy_conserved_from_friedmann · 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
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)
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_constant · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean
comoving_entropy_constant · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean:231 
/-- **Global adiabaticity.** If the equilibrium fluid satisfies the
continuity equation at every time, comoving entropy is the same at any two
times: `s(t₁)·a(t₁)³ = s(t₂)·a(t₂)³`. -/
theorem comoving_entropy_constant
    {ρ p s T a : ℝ → ℝ} {ρ' p' s' a' T' : ℝ → ℝ}
    (hTt : ∀ t, T t ≠ 0)
    (hρ : ∀ t, HasDerivAt ρ (ρ' t) t) (hp : ∀ t, HasDerivAt p (p' t) t)
    (hs : ∀ t, HasDerivAt s (s' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
    (hT : ∀ t, HasDerivAt T (T' t) t)
    (hEuler : ∀ u, T u * s u = ρ u + p u)
    (hGD : ∀ t, p' t = s t * T' t)
    (hcont : ∀ t, a t * ρ' t = -3 * a' t * (ρ t + p t))
    (t₁ t₂ : ℝ) :
    s t₁ * a t₁ ^ 3 = s t₂ * a t₂ ^ 3 := by
  have h0 : ∀ t, HasDerivAt (fun u => s u * a u ^ 3) 0 t := fun t =>
    comoving_entropy_conserved (hTt t) (hρ t) (hp t) (hs t) (ha t) (hT t)
      hEuler (hGD t) (hcont t)
  exact is_const_of_deriv_eq_zero (fun t => (h0 t).differentiableAt)
    (fun t => (h0 t).deriv) t₁ t₂
THEOREM radiation_aT_conserved · radiation_aT_constant · 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
radiation_aT_constant · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean:251 
/-- **Global free streaming.** If the decoupled radiation gas satisfies its
continuity equation at every time, `a·T` is the same at any two times. -/
theorem radiation_aT_constant
    {T a : ℝ → ℝ} {T' a' ρ' : ℝ → ℝ} {α : ℝ}
    (hα : α ≠ 0) (hTt : ∀ t, T t ≠ 0)
    (hT : ∀ t, HasDerivAt T (T' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
    (hρ : ∀ t, HasDerivAt (fun u => α * T u ^ 4) (ρ' t) t)
    (hcont : ∀ t, a t * ρ' t
        = -3 * a' t * (α * T t ^ 4 + α * T t ^ 4 / 3))
    (t₁ t₂ : ℝ) :
    a t₁ * T t₁ = a t₂ * T t₂ := by
  have h0 : ∀ t, HasDerivAt (fun u => a u * T u) 0 t := fun t =>
    radiation_aT_conserved hα (hTt t) (hT t) (ha t) (hρ t) (hcont t)
  exact is_const_of_deriv_eq_zero (fun t => (h0 t).differentiableAt)
    (fun t => (h0 t).deriv) t₁ t₂

What this page does not claim

The theorem does not prove the universe's expansion is adiabatic; it proves that adiabatic expansion follows from the Friedmann equations and local equilibrium. The theorem does not prove the neutrino gas is free streaming; it proves that free streaming follows from the continuity equation for a decoupled radiation gas. The theorem does not derive the Friedmann equations themselves; they remain the general relativistic input.

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