Encyclopedia Cosmology Cosmology Entropy Conservation Frw Radiation A T Conserved

ARTICLE 3 claims 3 theorems

Cosmology Entropy Conservation Frw Radiation A T Conserved

In an expanding universe, light from the early cosmos gets stretched to longer wavelengths; this page explains the precise sense in which that cooling is a forced consequence of Einstein's equations.

Verify this page

The redshift law

In cosmology, the temperature of the cosmic microwave background falls as the universe expands. The standard explanation is that the wavelength of each photon stretches with the scale factor, so the temperature drops inversely with the expansion. This page examines a precise, machine-checked derivation of that law from the equations of general relativity, and what it does and does not establish.

The classical starting point is the Friedmann equations, which govern the expansion of a homogeneous, isotropic universe. For a gas of radiation, with energy density proportional to the fourth power of temperature and pressure equal to one third of that density, the equations imply a simple relation: the product of the scale factor and the temperature stays constant. Equivalently, the temperature falls as one over the scale factor. This is the free-streaming redshift law, and it is the backbone of cosmic microwave background physics.

In the Recognition Science framework, the claim is not assumed but derived. The framework's machine-checked library of formal theorems proves that the continuity equation, which itself follows from the two Friedmann equations, forces the constancy of the scale factor times temperature. The theorem radiation_aT_conserved states that for a decoupled radiation gas, the derivative of the product is zero. The derivation uses only the radiation equation of state and the continuity equation; no separate postulate of adiabatic expansion or of free streaming is needed.

The significance is that a standard assumption of early universe cosmology is shown to be a theorem. The framework's library also upgrades this pointwise statement to a global one: the product of scale factor and temperature at any two times is equal. This global constancy is what cosmologists use when they trace the temperature of the cosmic microwave background back to the early universe.

What the theorem does not claim is equally important. It does not derive the Friedmann equations themselves; those are the general relativity input, taken as a model. It does not derive the equation of state for radiation; that is a separate physical assumption. It does not claim that the universe is actually radiation dominated at any given epoch. The theorem is conditional: if the Friedmann equations hold and the radiation gas is decoupled, then the redshift law follows. The framework's contribution is to show that the redshift law is a consequence of the dynamics, not an independent postulate.

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 continuity_from_friedmann · radiation_aT_conserved · 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
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 radiation_aT_constant · IndisputableMonolith/Cosmology/EntropyConservationFRW.lean
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 Friedmann equations themselves are derived from the framework. The radiation equation of state is derived from the framework. The universe is actually radiation dominated at any given epoch.

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