Without $\Lambda$ , a universe denser than critical cannot expand forever

Proved

CosmoConstCentury.supercritical_universe_recollapses

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

cosmologygeneral-relativitymathematical-physics

Let $G>0$ , $c>0$ , let $k$ be a real curvature index and $t_0$ a time. Let $R$ , $\rho$ be functions such that at time $t_0$ the density exceeds the critical density,

\rho(t_0)>\rho_c\big(H(t_0)\big)=\frac{3H(t_0)^2}{8\pi G},\qquad H=R'/R .

Then $(R,\rho)$ is not a solution of the Friedmann–Lemaître dust equations with $\Lambda=0$ and curvature index $k$ on the whole future half-line $[t_0,\infty)$ .

In other words, a supercritical universe without cosmological constant has a finite future: it cannot keep existing as a positive-radius solution for all later times, in line with the statement in Section 5.1 that such a cosmos would eventually collapse.

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 supercritical_universe_recollapses (G c k t₀ : ℝ) (hG : 0 < G) (hc : 0 < c)
    (R ρ : ℝ → ℝ) (hsuper : criticalDensity G (hubbleParam R t₀) < ρ t₀) :
    ¬ IsFriedmannSolution G c 0 k (Set.Ici 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 5.1, p. 85: with vanishing cosmological constant, a cosmos of density above critical is of spherical geometry and eventually collapses.

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,k,t_0$ be real numbers with $G>0$ , $c>0$ , and let $R,\rho:\mathbb R\to\mathbb R$ be any functions such that

\rho(t_0)>\frac{3H^2}{8\pi G},\qquad H=\frac{R'(t_0)}{R(t_0)}.

Conclusion: it is not the case that $(R,\rho)$ is a Friedmann solution with $\Lambda=0$ and curvature index $k$ on the half-line $[t_0,\infty)$ ; that is, it is not true that for every $t\ge t_0$ all of $R(t)>0$ , $R$ is $C^2$ near $t$ , $\dfrac{3R'(t)^2}{R(t)^2}+\dfrac{3kc^2}{R(t)^2}=\kappa c^2\rho(t)$ and $\dfrac{R'(t)^2}{R(t)^2}+\dfrac{2R''(t)}{R(t)}+\dfrac{kc^2}{R(t)^2}=0$ hold (with $\kappa=8\pi G/c^2$ ).

The density condition is imposed only at the single time $t_0$ . $k$ is an arbitrary real number (no assumption $k=1$ ). The statement is a non-existence claim; it does not describe how or when the solution ends.

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

Without Λ\LambdaΛ, a universe denser than critical cannot expand forever

Without $\Lambda$ , a universe denser than critical cannot expand forever