Lemaître's exponential form of the de Sitter universe (eq. 14): $R=e^{at}$ with $\rho=0$ , $k=0$ iff $\Lambda=3a^2$

Proved

CosmoConstCentury.lemaitre_exponential_de_sitter_iff

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

cosmologygeneral-relativitymathematical-physics

Let $a$ , $G$ , $c$ , $\Lambda$ be real constants. The empty ( $\rho\equiv0$ ), spatially flat ( $k=0$ ) universe with exponentially growing scale factor

R(t)=e^{at}

solves the Friedmann–Lemaître dust equations for all times if and only if

\Lambda=3a^2 .

This is the content of Lemaître's representation (14) of the de Sitter metric with a line element $e^{(\cdot)t}(-dx^2-dy^2-dz^2)+c^2dt^2$ : the de Sitter universe is not static, but expands exponentially at a rate fixed by the cosmological constant.

Formalization Note The predicate IsFriedmannSolution G c Λ k I R ρ requires, at every $t\in I$ , that $R(t)>0$ , that $R$ is $C^2$ in a neighbourhood of $t$ , and that the two equations hold with $\kappa=8\pi G/c^2$ . The review writes the metric factor as $e^{a\sqrt\lambda\,t}$ ; here the scale factor itself is $e^{at}$ with a free rate $a$ , and the theorem determines the relation between that rate and $\Lambda$ .

Preamble

import Mathlib
import Definitions.Def_CosmoConstCentury_Defs

open Filter Topology

Formal statement

namespace CosmoConstCentury

theorem lemaitre_exponential_de_sitter_iff (G c Λ a : ℝ) :
    IsFriedmannSolution G c Λ 0 Set.univ (fun t => Real.exp (a * t)) (fun _ => 0) ↔
      Λ = 3 * a ^ 2 := by sorry

end CosmoConstCentury

Source

C. O'Raifeartaigh, M. O'Keeffe, W. Nahm, S. Mitton, "One hundred years of the cosmological constant: from 'superfluous stunt' to dark energy", Eur. Phys. J. H 43, 73-117 (2018), https://doi.org/10.1140/epjh/e2017-80061-7; Section 3.2, p. 81, eq. (14) (Lemaître 1925); equations (15)-(16) p. 82 with k = 0.

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Disclosure: non-blind read-back. This read-back was written by the same agent that drafted the Lean statement (Aristotle, by Harmonic), at the explicit request of the proposal owner. It is not an independent or blind audit, and it must not be treated as independent testimony: its author knew the source paper and the intended meaning while writing it. Reviewers should compare it against the Lean code themselves.

Let $G,c,\Lambda,a$ be arbitrary real numbers. The statement asserts the equivalence of:

the functions $R(t)=e^{at}$ and $\rho(t)=0$ form a Friedmann solution with curvature index $k=0$ on the whole real line: for every real $t$ , $R(t)>0$ , $R$ is $C^2$ near $t$ , and (with $R'/R=a$ , $R''/R=a^2$ )

3a^2-\Lambda=0,\qquad a^2+2a^2-\Lambda=0;

$\Lambda=3a^2$ .

The case $a=0$ is included (static flat empty universe, $\Lambda=0$ ). The sign of $a$ is not restricted, so contracting exponentials are included as well.

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemaître's exponential form of the de Sitter universe (eq. 14): R=eatR=e^{at}R=eat with ρ=0\rho=0ρ=0, k=0k=0k=0 iff Λ=3a2\Lambda=3a^2Λ=3a2

Lemaître's exponential form of the de Sitter universe (eq. 14): $R=e^{at}$ with $\rho=0$ , $k=0$ iff $\Lambda=3a^2$