Einstein's static universe (eq. 10): $\Lambda=\kappa c^2\rho/2=c^2/R^2$

Proved

CosmoConstCentury.einstein_static_universe_iff

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

cosmologygeneral-relativitymathematical-physics

Let $R_0>0$ and $\rho_0$ be constants, and let $G$ , $c$ , $\Lambda$ be arbitrary real constants with $\kappa=8\pi G/c^2$ . The constant scale factor $R(t)\equiv R_0$ together with the constant density $\rho(t)\equiv\rho_0$ solves the closed ( $k=1$ ) Friedmann–Lemaître dust equations (15)–(16) for all times if and only if

\Lambda=\frac{\kappa c^2\rho_0}{2}\qquad\text{and}\qquad\Lambda=\frac{c^2}{R_0^2}.

In units with $c=1$ this is Einstein's 1917 relation (10), $\lambda=\kappa\rho/2=1/R^2$ , linking the cosmological constant, the mean density and the radius of the static closed universe.

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_iff (G c Λ R₀ ρ₀ : ℝ) (hR₀ : 0 < R₀) :
    IsFriedmannSolution G c Λ 1 Set.univ (fun _ => R₀) (fun _ => ρ₀) ↔
      (Λ = einsteinKappa G c * c ^ 2 * ρ₀ / 2 ∧ Λ = c ^ 2 / R₀ ^ 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, p. 78, eq. (10) (Einstein 1917); field equations (9) p. 77; Friedmann form (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 $R_0>0$ (no sign conditions on $G$ , $c$ , $\Lambda$ , $\rho_0$ ). Write $\kappa=8\pi G/c^2$ (which is $0$ if $c=0$ ). The statement asserts the equivalence of:

the constant functions $R(t)=R_0$ and $\rho(t)=\rho_0$ form a Friedmann solution with curvature index $k=1$ on the whole real line, i.e. for every real $t$ : $R_0>0$ , $R$ is $C^2$ near $t$ , and (since $R'=R''=0$ )

\frac{3c^2}{R_0^2}-\Lambda=\kappa c^2\rho_0,\qquad \frac{c^2}{R_0^2}-\Lambda=0;

$\Lambda=\dfrac{\kappa c^2\rho_0}{2}$ and $\Lambda=\dfrac{c^2}{R_0^2}$ .

View graph

Einstein's static universe (eq. 10): Λ=κc2ρ/2=c2/R2\Lambda=\kappa c^2\rho/2=c^2/R^2Λ=κc2ρ/2=c2/R2

Einstein's static universe (eq. 10): $\Lambda=\kappa c^2\rho/2=c^2/R^2$