Eddington: Einstein's static universe is unstable

Proved

CosmoConstCentury.einstein_static_universe_unstable

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

cosmologygeneral-relativitymathematical-physics

Let $G>0$ , $c>0$ , and let $R_0>0$ , $\rho_0$ be such that the constant pair $(R_0,\rho_0)$ is a static solution of the closed ( $k=1$ ) Friedmann–Lemaître dust equations (15)–(16) with cosmological constant $\Lambda$ (Einstein's static universe). Then this solution is unstable: there is $\delta>0$ such that for every $\varepsilon>0$ there exist a time $T>0$ and a solution $(R,\rho)$ of the same equations, with the same $\Lambda$ , on the time interval $[0,T]$ , such that

|R(0)-R_0|<\varepsilon,\qquad |R'(0)|<\varepsilon,\qquad |\rho(0)-\rho_0|<\varepsilon,

but

|R(T)-R_0|\ge\delta .

This is the instability described in Section 3.1 (Eddington 1930): an arbitrarily small perturbation of the Einstein world drives it away from the static state, into contraction or runaway expansion.

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$ .

Preamble

import Mathlib
import Definitions.Def_CosmoConstCentury_Defs

open Filter Topology

Formal statement

namespace CosmoConstCentury

theorem einstein_static_universe_unstable (G c Λ R₀ ρ₀ : ℝ) (hG : 0 < G) (hc : 0 < c)
    (hR₀ : 0 < R₀)
    (hstatic : IsFriedmannSolution G c Λ 1 Set.univ (fun _ => R₀) (fun _ => ρ₀)) :
    ∃ δ > 0, ∀ ε > 0, ∃ (R ρ : ℝ → ℝ) (T : ℝ), 0 < T ∧
      IsFriedmannSolution G c Λ 1 (Set.Icc 0 T) R ρ ∧
      |R 0 - R₀| < ε ∧ |deriv R 0| < ε ∧ |ρ 0 - ρ₀| < ε ∧ δ ≤ |R T - R₀| := 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.1, pp. 80-81 (Eddington 1930, 1933); static solution eq. (10) p. 78; equations (15)-(16) p. 82.

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,R_0,\rho_0$ be real numbers with $G>0$ , $c>0$ , $R_0>0$ , and assume that the constant functions $R\equiv R_0$ , $\rho\equiv\rho_0$ form a Friedmann solution with $k=1$ on the whole real line (for every $t$ : $\dfrac{3c^2}{R_0^2}-\Lambda=\kappa c^2\rho_0$ and $\dfrac{c^2}{R_0^2}-\Lambda=0$ , with $\kappa=8\pi G/c^2$ ).

Conclusion: there exists $\delta>0$ such that for every $\varepsilon>0$ there exist functions $R,\rho:\mathbb R\to\mathbb R$ and a real $T>0$ with:

$(R,\rho)$ is a Friedmann solution with the same $G,c,\Lambda$ and $k=1$ on the closed interval $[0,T]$ : for every $t\in[0,T]$ , $R(t)>0$ , $R$ is $C^2$ near $t$ , $\dfrac{3R'(t)^2}{R(t)^2}+\dfrac{3c^2}{R(t)^2}-\Lambda=\kappa c^2\rho(t)$ and $\dfrac{R'(t)^2}{R(t)^2}+\dfrac{2R''(t)}{R(t)}+\dfrac{c^2}{R(t)^2}-\Lambda=0$ ;
$|R(0)-R_0|<\varepsilon$ , $|R'(0)|<\varepsilon$ and $|\rho(0)-\rho_0|<\varepsilon$ ;
$|R(T)-R_0|\ge\delta$ .

The order of quantifiers is: $\delta$ first, independent of $\varepsilon$ ; then for each $\varepsilon$ a solution and a time $T$ depending on $\varepsilon$ . The perturbed solution is only required to exist on $[0,T]$ ; nothing is said about its behaviour after $T$ , nor about the direction (expansion or contraction) of the departure.

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