Energy density scales as $a^{-3(1+w)}$

Proved

CosmologyEOS.energy_density_scaling

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

cosmologymathematical-physics

Let $I\subseteq\mathbb R$ be an open, connected set of times and let $w\in\mathbb R$ . Let $a,\varepsilon,p$ be real functions of time such that on $I$ : $a$ and $\varepsilon$ are differentiable, $a>0$ , the fluid has constant equation of state $p = w\varepsilon$ , and the fluid equation $\dot\varepsilon = -3\frac{\dot a}{a}(\varepsilon + p)$ holds. Then for all $s,t\in I$

\varepsilon(t)\,a(t)^{3(1+w)} = \varepsilon(s)\,a(s)^{3(1+w)},

i.e. $\varepsilon \propto a^{-3(1+w)}$ .

This is the basic dilution law of a perfect fluid in an FLRW universe; every special case in the source (dust, radiation, stiff matter, cosmological constant) is an instance.

Formalization Note The power $a^{3(1+w)}$ is a real power (Real.rpow) of the positive number $a$ . No sign condition on $\varepsilon$ is assumed.

Preamble

import Mathlib
import Definitions.Def_CosmologyEOS_Defs

open Real Filter Topology

Formal statement

namespace CosmologyEOS

theorem energy_density_scaling (w : ℝ) (a ε p : ℝ → ℝ) (I : Set ℝ)
    (hI_open : IsOpen I) (hI_conn : IsPreconnected I)
    (ha_diff : ∀ t ∈ I, DifferentiableAt ℝ a t)
    (hε_diff : ∀ t ∈ I, DifferentiableAt ℝ ε t)
    (ha_pos : ∀ t ∈ I, 0 < a t)
    (heos : ∀ t ∈ I, p t = w * ε t)
    (hfluid : ∀ t ∈ I, FluidEquation a ε p t) :
    ∀ s ∈ I, ∀ t ∈ I,
      ε t * a t ^ (3 * (1 + w)) = ε s * a s ^ (3 * (1 + w)) := by
  sorry

end CosmologyEOS

Source

Wikipedia, "Equation of state (cosmology)", revision 1375011367, https://en.wikipedia.org/w/index.php?title=Equation_of_state_(cosmology)&oldid=1375011367, section 'FLRW equations and the equation of state' (ε ∝ a^{-3(1+w)})

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; NON-BLIND

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent that drafted the Lean statement below, with full knowledge of the source text and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; reviewers should compare the Lean code with the source themselves.

Let $w\in\mathbb R$ , let $a,\varepsilon,p:\mathbb R\to\mathbb R$ and let $I\subseteq\mathbb R$ be a set that is open and preconnected (preconnected allows $I = \emptyset$ , in which case the statement is vacuous). Assume that for every $t\in I$ : $a$ is differentiable at $t$ ; $\varepsilon$ is differentiable at $t$ ; $a(t)>0$ ; $p(t) = w\,\varepsilon(t)$ ; and $\varepsilon^{\prime}(t) = -3\,\dfrac{a^{\prime}(t)}{a(t)}\,(\varepsilon(t)+p(t))$ . Then for all $s,t\in I$ ,

\varepsilon(t)\,a(t)^{3(1+w)} = \varepsilon(s)\,a(s)^{3(1+w)},

where $x^{y}$ is the real power $\exp(y\log x)$ (well defined since $a>0$ on $I$ ). No hypothesis is made on $p$ or $\varepsilon$ outside $I$ , on the sign of $\varepsilon$ , or on $w$ .

Human review

Endorsed by marwahaha · Oct 21, 2026

View graph

Energy density scales as a−3(1+w)a^{-3(1+w)}a−3(1+w)

Energy density scales as $a^{-3(1+w)}$