Critical density decides the curvature: $k=0 \iff \rho=\rho_c$ , $k>0\iff\rho>\rho_c$ , $k<0\iff\rho<\rho_c$ (for $\Lambda=0$ )

Proved

FriedmannEquations.curvature_sign_iff_critical_density

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

cosmologyfriedmann-equationsgeneral-relativity

Let $G > 0$ , $k\in\mathbb R$ , and suppose that at a time $t$ with $R(t)\neq 0$ the first Friedmann equation with vanishing cosmological constant holds:

H^2 = \frac{8\pi G\rho}{3} - \frac{k}{R^2},\qquad H = \dot R/R.

With the critical density $\rho_c = \dfrac{3H^2}{8\pi G}$ of this Hubble rate,

k = 0 \iff \rho = \rho_c,\qquad k > 0 \iff \rho > \rho_c,\qquad k < 0 \iff \rho < \rho_c,

i.e. critical density gives a flat universe, higher density a closed one ( $k>0$ ) and lower density an open one ( $k<0$ ).

Preamble

import Definitions.Def_FriedmannEquations_Defs
import Mathlib

open FriedmannEquations

Formal statement

theorem FriedmannEquations.curvature_sign_iff_critical_density
    (G k : ℝ) (hG : 0 < G) (R ρ : ℝ → ℝ) (t : ℝ) (hR : R t ≠ 0)
    (h₁ : FirstFriedmannEq G 0 k R ρ t) :
    (k = 0 ↔ ρ t = criticalDensity G (hubble R t)) ∧
    (0 < k ↔ criticalDensity G (hubble R t) < ρ t) ∧
    (k < 0 ↔ ρ t < criticalDensity G (hubble R t)) := by sorry

Source

Wikipedia, "Friedmann equations", revision oldid=1374073387, https://en.wikipedia.org/w/index.php?title=Friedmann_equations&oldid=1374073387 (the PDF supplied with this proposal), sections "Spatial curvature" (pp. 2–3) and "Critical density" (p. 3).

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

NOTE — NON-BLIND READ-BACK. This read-back is not independent testimony. It was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source article and of the intended meaning. It was produced at the explicit request of the proposal owner. Reviewers must not treat it as a blind audit; an independent read-back is still recommended.

Fix reals $G,k$ with $G>0$ , functions $R,\rho:\mathbb R\to\mathbb R$ and a time $t\in\mathbb R$ with $R(t)\neq0$ . Assume at this single time $t$

\Big(\frac{\dot R(t)}{R(t)}\Big)^2 = \frac{8\pi G\rho(t)}{3} - \frac{k}{R(t)^2} + \frac{0}{3}

(the first Friedmann equation with $\Lambda = 0$ ; $\dot R(t)$ is deriv, junk $0$ if $R$ is not differentiable at $t$ ). Write $H = \dot R(t)/R(t)$ and $\rho_c = 3H^2/(8\pi G)$ . Conclusion: all three of

k=0\iff \rho(t)=\rho_c,\qquad 0<k\iff \rho_c<\rho(t),\qquad k<0\iff \rho(t)<\rho_c

hold. Nothing is assumed at other times, and no differentiability is assumed.

View graph

Critical density decides the curvature: k=0 ⟺ ρ=ρck=0 \iff \rho=\rho_ck=0⟺ρ=ρc​, k>0 ⟺ ρ>ρck>0\iff\rho>\rho_ck>0⟺ρ>ρc​, k<0 ⟺ ρ<ρck<0\iff\rho<\rho_ck<0⟺ρ<ρc​ (for Λ=0\Lambda=0Λ=0)

Critical density decides the curvature: $k=0 \iff \rho=\rho_c$ , $k>0\iff\rho>\rho_c$ , $k<0\iff\rho<\rho_c$ (for $\Lambda=0$ )