First Friedmann equation in density parameters: $H^2/H_0^2 = \Omega_{0,R}a^{-4} + \Omega_{0,M}a^{-3} + \Omega_{0,k}a^{-2} + \Omega_{0,\Lambda}$

Proved

FriedmannEquations.first_friedmann_density_parameters

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

cosmologyfriedmann-equationsgeneral-relativity

Let $G>0$ and $\Lambda,k\in\mathbb R$ ; let $t_0$ ("today") and $t$ be times with $R(t_0)\ne 0$ , $R(t)\ne0$ and $H_0 := H(t_0)\neq 0$ , and let $a = R(t)/R(t_0)$ . Suppose the density consists of radiation and matter, $\rho(s) = \rho_R\,a(s)^{-4} + \rho_M\,a(s)^{-3}$ for all $s$ (with $a(s)=R(s)/R(t_0)$ ), and that the first Friedmann equation $H^2 = \frac{8\pi G\rho}{3} - \frac{k}{R^2} + \frac{\Lambda}{3}$ holds at $t$ and at $t_0$ . With the present-day density parameters

\Omega_{0,R} = \frac{\rho_R}{\rho_c},\quad \Omega_{0,M} = \frac{\rho_M}{\rho_c},\quad \Omega_{0,\Lambda} = \frac{\Lambda/(8\pi G)}{\rho_c} = \frac{\Lambda}{3H_0^2},\quad \Omega_{0,k} = 1 - \Omega_0,\ \ \Omega_0 = \Omega_{0,R}+\Omega_{0,M}+\Omega_{0,\Lambda},

where $\rho_c = 3H_0^2/(8\pi G)$ , one has

\frac{H(t)^2}{H_0^2} = \Omega_{0,R}a^{-4} + \Omega_{0,M}a^{-3} + \Omega_{0,k}a^{-2} + \Omega_{0,\Lambda}.

Here the vacuum energy is counted in the total $\Omega_0$ (vacuum density $\Lambda/8\pi G$ , cf. section Cosmological constant).

Preamble

import Definitions.Def_FriedmannEquations_Defs
import Mathlib

open FriedmannEquations

Formal statement

theorem FriedmannEquations.first_friedmann_density_parameters
    (G Λ k ρR ρM : ℝ) (hG : 0 < G) (R ρ : ℝ → ℝ) (t t₀ : ℝ)
    (hR : R t ≠ 0) (hR₀ : R t₀ ≠ 0) (hH₀ : hubble R t₀ ≠ 0)
    (hρ : ∀ s, ρ s = ρR / (R s / R t₀) ^ 4 + ρM / (R s / R t₀) ^ 3)
    (h₁ : FirstFriedmannEq G Λ k R ρ t) (h₁₀ : FirstFriedmannEq G Λ k R ρ t₀) :
    let a := R t / R t₀
    let H₀ := hubble R t₀
    let ΩR := densityParameter G H₀ ρR
    let ΩM := densityParameter G H₀ ρM
    let ΩΛ := densityParameter G H₀ (Λ / (8 * Real.pi * G))
    let Ωk := 1 - (ΩR + ΩM + ΩΛ)
    hubble R t ^ 2 / H₀ ^ 2 =
      ΩR * a ^ (-4 : ℤ) + ΩM * a ^ (-3 : ℤ) + Ωk * a ^ (-2 : ℤ) + ΩΛ := 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), section "Density parameter", p. 5 (display after "in terms of the present values of the density parameters").

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,\Lambda,k,\rho_R,\rho_M$ with $G>0$ , functions $R,\rho:\mathbb R\to\mathbb R$ and times $t,t_0$ . Assume $R(t)\neq0$ , $R(t_0)\ne0$ , and $H_0 := \dot R(t_0)/R(t_0)\neq 0$ ; assume for every real $s$ ,

\rho(s) = \frac{\rho_R}{(R(s)/R(t_0))^4} + \frac{\rho_M}{(R(s)/R(t_0))^3}

(junk: division by $0$ gives $0$ where $R(s)=0$ ); and assume at $t$ and at $t_0$ (same $k$ , $\Lambda$ )

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

Define $a = R(t)/R(t_0)$ , $\rho_c = 3H_0^2/(8\pi G)$ , $\Omega_R = \rho_R/\rho_c$ , $\Omega_M = \rho_M/\rho_c$ , $\Omega_\Lambda = \big(\Lambda/(8\pi G)\big)/\rho_c$ , $\Omega_k = 1-(\Omega_R+\Omega_M+\Omega_\Lambda)$ . Conclusion:

\frac{(\dot R(t)/R(t))^2}{H_0^2} = \Omega_R\,a^{-4} + \Omega_M\,a^{-3} + \Omega_k\,a^{-2} + \Omega_\Lambda,

with integer powers $a^{-n}$ .

View graph

First Friedmann equation in density parameters: H2/H02=Ω0,Ra−4+Ω0,Ma−3+Ω0,ka−2+Ω0,ΛH^2/H_0^2 = \Omega_{0,R}a^{-4} + \Omega_{0,M}a^{-3} + \Omega_{0,k}a^{-2} + \Omega_{0,\Lambda}H2/H02​=Ω0,R​a−4+Ω0,M​a−3+Ω0,k​a−2+Ω0,Λ​

First Friedmann equation in density parameters: $H^2/H_0^2 = \Omega_{0,R}a^{-4} + \Omega_{0,M}a^{-3} + \Omega_{0,k}a^{-2} + \Omega_{0,\Lambda}$