Flat universe dominated by one fluid: $a \propto t^{2/(3(1+w))}$

Proved

CosmologyEOS.flat_universe_power_law

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

cosmologymathematical-physics

Let $G>0$ be Newton's constant and let $w>-1$ . Let $a,\varepsilon,p$ be real functions of time such that for every $t>0$ : $a$ and $\varepsilon$ are differentiable at $t$ , $a(t)>0$ , $p(t) = w\,\varepsilon(t)$ , the fluid equation $\dot\varepsilon = -3\frac{\dot a}{a}(\varepsilon+p)$ holds, and the flat Friedmann equation $\left(\frac{\dot a}{a}\right)^2 = \frac{8\pi G}{3}\varepsilon$ holds. Suppose the universe starts from a big bang at $t = 0$ , i.e. $a(t)\to 0$ as $t\to 0^+$ . Then there is a constant $C>0$ such that

a(t) = C\,t^{\frac{2}{3(1+w)}}\qquad\text{for all } t>0.

This is the source's statement that, if the fluid is the dominant form of matter in a flat universe, $a\propto t^{2/(3(1+w))}$ , where $t$ is the proper time.

Formalization Note The proportionality is normalized by placing the big bang at $t=0$ . Neither monotonicity of $a$ nor positivity of $\varepsilon$ is assumed; the hypothesis $w>-1$ is where the source's exponent is defined (the case $w=-1$ is treated separately).

Preamble

import Mathlib
import Definitions.Def_CosmologyEOS_Defs

open Real Filter Topology

Formal statement

namespace CosmologyEOS

theorem flat_universe_power_law (G w : ℝ) (hG : 0 < G) (hw : -1 < w) (a ε p : ℝ → ℝ)
    (ha_diff : ∀ t > 0, DifferentiableAt ℝ a t)
    (hε_diff : ∀ t > 0, DifferentiableAt ℝ ε t)
    (ha_pos : ∀ t > 0, 0 < a t)
    (heos : ∀ t > 0, p t = w * ε t)
    (hfluid : ∀ t > 0, FluidEquation a ε p t)
    (hfried : ∀ t > 0, FlatFriedmannEquation G a ε t)
    (hbang : Tendsto a (𝓝[>] 0) (𝓝 0)) :
    ∃ C > 0, ∀ t > 0, a t = C * t ^ (2 / (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 ∝ t^{2/(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 $G, w\in\mathbb R$ with $G>0$ and $w>-1$ , and let $a,\varepsilon,p:\mathbb R\to\mathbb R$ . Assume that for every real $t>0$ : $a$ is differentiable at $t$ ; $\varepsilon$ is differentiable at $t$ ; $a(t)>0$ ; $p(t) = w\,\varepsilon(t)$ ; $\varepsilon^{\prime}(t) = -3\,\dfrac{a^{\prime}(t)}{a(t)}(\varepsilon(t)+p(t))$ ; and $\left(\dfrac{a^{\prime}(t)}{a(t)}\right)^2 = \dfrac{8\pi G}{3}\,\varepsilon(t)$ . Assume further that $a(t)\to 0$ as $t\to 0$ from the right (only values at $t>0$ matter; $a(0)$ is unconstrained). Then there exists a real $C>0$ such that for every $t>0$ ,

a(t) = C\cdot t^{\frac{2}{3(1+w)}},

with the real power. Nothing is assumed about the functions for $t\le 0$ , about the sign of $\varepsilon$ , or about the monotonicity of $a$ .

Human review

Endorsed by marwahaha · Oct 21, 2026

View graph

Flat universe dominated by one fluid: a∝t2/(3(1+w))a \propto t^{2/(3(1+w))}a∝t2/(3(1+w))

Flat universe dominated by one fluid: $a \propto t^{2/(3(1+w))}$