De Sitter's empty "Solution B" (eq. 13): $\rho=0$ , $\Lambda=3c^2/R_0^2$

Proved

CosmoConstCentury.de_sitter_solution_B_iff

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

cosmologygeneral-relativitymathematical-physics

Let $R_0>0$ and let $G$ , $c$ , $\Lambda$ be real constants. Consider the empty universe ( $\rho\equiv0$ ) with scale factor

R(t)=R_0\cosh\!\Big(\frac{ct}{R_0}\Big).

This pair solves the closed ( $k=1$ ) Friedmann–Lemaître dust equations (15)–(16) for all times if and only if

\Lambda=\frac{3c^2}{R_0^2}.

In units with $c=1$ this is de Sitter's 1917 "Solution B", $\rho=0$ , $\lambda=3/R^2$ (13), written in the closed slicing in which de Sitter space appears as a Friedmann universe of minimal radius $R_0$ .

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$ . De Sitter's original static coordinates are not used; the cosh form is the representation of the same empty solution in the closed Friedmann slicing.

Preamble

import Mathlib
import Definitions.Def_CosmoConstCentury_Defs

open Filter Topology

Formal statement

namespace CosmoConstCentury

theorem de_sitter_solution_B_iff (G c Λ R₀ : ℝ) (hR₀ : 0 < R₀) :
    IsFriedmannSolution G c Λ 1 Set.univ (fun t => R₀ * Real.cosh (c * t / R₀)) (fun _ => 0) ↔
      Λ = 3 * 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.2, p. 81, eqs. (12)-(13) (de Sitter 1917); 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$ be real numbers with $R_0>0$ (no conditions on $G$ , $c$ , $\Lambda$ ). The statement asserts the equivalence of:

the functions $R(t)=R_0\cosh(ct/R_0)$ and $\rho(t)=0$ form a Friedmann solution with $k=1$ on the whole real line: for every real $t$ , $R(t)>0$ , $R$ is $C^2$ near $t$ , and

\frac{3R'(t)^2}{R(t)^2}+\frac{3c^2}{R(t)^2}-\Lambda=0,\qquad \frac{R'(t)^2}{R(t)^2}+\frac{2R''(t)}{R(t)}+\frac{c^2}{R(t)^2}-\Lambda=0

(the right side of the first equation is $\kappa c^2\cdot 0=0$ ); 2. $\Lambda=\dfrac{3c^2}{R_0^2}$ .

Because the density is identically zero, $G$ plays no role. If $c=0$ the scale factor is the constant $R_0$ and condition 2 reads $\Lambda=0$ .

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

De Sitter's empty "Solution B" (eq. 13): ρ=0\rho=0ρ=0, Λ=3c2/R02\Lambda=3c^2/R_0^2Λ=3c2/R02​

De Sitter's empty "Solution B" (eq. 13): $\rho=0$ , $\Lambda=3c^2/R_0^2$