Prove2Me

Non-relativistic matter: ε∝a−3\varepsilon \propto a^{-3}

Proved
CosmologyEOS.dust_energy_density_scaling

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

cosmologymathematical-physics

Let I⊆RI\subseteq\mathbb R be an open, connected set of times and let a,ε,pa,\varepsilon,p be real functions of time such that on II: aa and ε\varepsilon are differentiable, a>0a>0, the equation of state is p=0 εp = 0\,\varepsilon, and the fluid equation ε˙=−3a˙a(ε+p)\dot\varepsilon = -3\frac{\dot a}{a}(\varepsilon + p) holds. Then for all s,t∈Is,t\in I

ε(t) a(t)3=ε(s) a(s)3,\varepsilon(t)\,a(t)^{3} = \varepsilon(s)\,a(s)^{3},

i.e. ε∝a−3\varepsilon \propto a^{-3}.

This is the non-relativistic matter case of the general scaling law ε∝a−3(1+w)\varepsilon\propto a^{-3(1+w)}.

Preamble
import Mathlib
import Definitions.Def_CosmologyEOS_Defs

open Real Filter Topology
Formal statement
namespace CosmologyEOS

theorem dust_energy_density_scaling (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 = 0 * ε t)
    (hfluid : ∀ t ∈ I, FluidEquation a ε p t) :
    ∀ s ∈ I, ∀ t ∈ I, ε t * a t ^ 3 = ε s * a s ^ 3 := 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 'Non-relativistic particles'
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 a,ε,p:R→Ra,\varepsilon,p:\mathbb R\to\mathbb R and let I⊆RI\subseteq\mathbb R be open and preconnected (possibly empty, in which case the statement is vacuous). Assume that for every t∈It\in I: aa and ε\varepsilon are differentiable at tt; a(t)>0a(t)>0; p(t)=0⋅ε(t)p(t) = 0\cdot\varepsilon(t); and ε′(t)=−3 a′(t)a(t) (ε(t)+p(t))\varepsilon^{\prime}(t) = -3\,\dfrac{a^{\prime}(t)}{a(t)}\,(\varepsilon(t)+p(t)). Then for all s,t∈Is,t\in I,

ε(t) a(t)3=ε(s) a(s)3,\varepsilon(t)\,a(t)^{3} = \varepsilon(s)\,a(s)^{3},

with an ordinary natural-number power 33. Nothing is assumed about the sign of ε\varepsilon or about the functions outside II.

Human review

View graph