Prove2Me

Cosmological constant w=−1w=-1: a∝eHta \propto e^{Ht}

Proved
CosmologyEOS.cosmological_constant_exponential_expansion

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

cosmologymathematical-physics

Let G>0G>0 and let a,ε,pa,\varepsilon,p be real functions of time, differentiable everywhere, with a>0a>0, equation of state p=−εp = -\varepsilon (i.e. w=−1w=-1), satisfying the fluid equation ε˙=−3a˙a(ε+p)\dot\varepsilon = -3\frac{\dot a}{a}(\varepsilon+p) and the flat Friedmann equation (a˙a)2=8πG3ε\left(\frac{\dot a}{a}\right)^2 = \frac{8\pi G}{3}\varepsilon at all times. Then the energy density is constant and the scale factor is exponential: there are constants HH and C>0C>0 with

H2=8πG3 ε(0),a(t)=C eHt,ε(t)=ε(0)for all t∈R.H^2 = \frac{8\pi G}{3}\,\varepsilon(0),\qquad a(t) = C\,e^{Ht},\qquad \varepsilon(t) = \varepsilon(0)\quad\text{for all } t\in\mathbb R.

Here HH is the Hubble parameter.

Formalization Note HH is allowed to have either sign (an expanding or contracting de Sitter solution); the source's expanding case is H>0H>0.

Preamble
import Mathlib
import Definitions.Def_CosmologyEOS_Defs

open Real Filter Topology
Formal statement
namespace CosmologyEOS

theorem cosmological_constant_exponential_expansion (G : ℝ) (hG : 0 < G) (a ε p : ℝ → ℝ)
    (ha_diff : ∀ t, DifferentiableAt ℝ a t)
    (hε_diff : ∀ t, DifferentiableAt ℝ ε t)
    (ha_pos : ∀ t, 0 < a t)
    (heos : ∀ t, p t = -1 * ε t)
    (hfluid : ∀ t, FluidEquation a ε p t)
    (hfried : ∀ t, FlatFriedmannEquation G a ε t) :
    ∃ H C : ℝ, 0 < C ∧ H ^ 2 = 8 * π * G / 3 * ε 0 ∧
      ∀ t, a t = C * Real.exp (H * t) ∧ ε t = ε 0 := 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 'Acceleration of cosmic inflation' (w = −1, a ∝ e^{Ht})
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>0G>0 and a,ε,p:R→Ra,\varepsilon,p:\mathbb R\to\mathbb R. Assume for every t∈Rt\in\mathbb R: aa and ε\varepsilon are differentiable at tt; a(t)>0a(t)>0; p(t)=−1⋅ε(t)p(t) = -1\cdot\varepsilon(t); ε′(t)=−3 a′(t)a(t)(ε(t)+p(t))\varepsilon^{\prime}(t) = -3\,\dfrac{a^{\prime}(t)}{a(t)}(\varepsilon(t)+p(t)); and (a′(t)a(t))2=8πG3ε(t)\left(\dfrac{a^{\prime}(t)}{a(t)}\right)^2 = \dfrac{8\pi G}{3}\varepsilon(t). Then there exist real numbers HH and CC with C>0C>0, H2=8πG3 ε(0)H^2 = \dfrac{8\pi G}{3}\,\varepsilon(0), and, for every t∈Rt\in\mathbb R, both a(t)=C eHta(t) = C\,e^{Ht} and ε(t)=ε(0)\varepsilon(t) = \varepsilon(0). The sign of HH is not specified, and ε(0)\varepsilon(0) is not assumed positive (if ε(0)<0\varepsilon(0)<0 the hypotheses cannot all hold).

Human review

View graph