Critical density decides the spatial curvature when $\Lambda=0$

Proved

CosmoConstCentury.critical_density_classification

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 let $(R,\rho)$ solve the Friedmann–Lemaître dust equations with vanishing cosmological constant ( $\Lambda=0$ ) and curvature index $k$ on a set of times $I$ . At every $t\in I$ , with $H=R'/R$ and the critical density $\rho_c=3H^2/(8\pi G)$ :

$k>0$ (spherical geometry) if and only if $\rho>\rho_c$ ;
$k=0$ (Euclidean geometry) if and only if $\rho=\rho_c$ ;
$k<0$ (hyperbolic geometry) if and only if $\rho<\rho_c$ .

This is the classification of cosmic models by the density parameter $\Omega=\rho/\rho_c$ described in Section 5.1, with the Einstein–de Sitter universe as the critical case.

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 critical_density_classification (G c k : ℝ) (hG : 0 < G) (hc : 0 < c) (I : Set ℝ)
    (R ρ : ℝ → ℝ) (hsol : IsFriedmannSolution G c 0 k I R ρ) (t : ℝ) (ht : t ∈ I) :
    (0 < k ↔ criticalDensity G (hubbleParam R t) < ρ t) ∧
    (k = 0 ↔ ρ t = criticalDensity G (hubbleParam R t)) ∧
    (k < 0 ↔ ρ t < criticalDensity G (hubbleParam R t)) := 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, critical density rho_c = 3H0^2/8piG from eq. (18) and the classification that follows.

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$ be real numbers with $G>0$ and $c>0$ ; let $I\subseteq\mathbb R$ be any set and let $R,\rho$ form a Friedmann solution with $\Lambda=0$ and curvature index $k$ on $I$ (for every $s\in I$ : $R(s)>0$ , $R$ is $C^2$ near $s$ , $\dfrac{3R'(s)^2}{R(s)^2}+\dfrac{3kc^2}{R(s)^2}=\kappa c^2\rho(s)$ and $\dfrac{R'(s)^2}{R(s)^2}+\dfrac{2R''(s)}{R(s)}+\dfrac{kc^2}{R(s)^2}=0$ , $\kappa=8\pi G/c^2$ ). Let $t\in I$ , and put $H=R'(t)/R(t)$ and $\rho_c=\dfrac{3H^2}{8\pi G}$ . Then all three hold:

$0<k$ if and only if $\rho_c<\rho(t)$ ;
$k=0$ if and only if $\rho(t)=\rho_c$ ;
$k<0$ if and only if $\rho(t)<\rho_c$ .

$k$ is any real number, not only $-1,0,1$ . The case $H=0$ is included, where $\rho_c=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

Critical density decides the spatial curvature when Λ=0\Lambda=0Λ=0

Critical density decides the spatial curvature when $\Lambda=0$