First Friedmann equation in the dimensionless scale factor: $H^2 = (\dot a/a)^2 = \frac{8\pi G}{3}\big[\rho + \frac{\rho_c-\rho_0}{a^2}\big]$

Proved

FriedmannEquations.first_friedmann_dimensionless

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

cosmologyfriedmann-equationsgeneral-relativity

Let $G>0$ , $k\in\mathbb R$ , and let $t_0$ ("now") and $t$ be times with $R(t_0)\ne0$ , $R(t)\neq 0$ . Suppose the first Friedmann equation with $\Lambda = 0$ , $H^2 = \frac{8\pi G\rho}{3} - \frac{k}{R^2}$ , holds at both $t$ and $t_0$ (same $k$ ). Put $a(s) = R(s)/R(t_0)$ , $H_0 = H(t_0)$ , $\rho_0 = \rho(t_0)$ and $\rho_c = 3H_0^2/(8\pi G)$ . Then $\dot a(t)/a(t) = H(t)$ and

\Big(\frac{\dot a(t)}{a(t)}\Big)^2 = \frac{8\pi G}{3}\left[\rho(t) + \frac{\rho_c - \rho_0}{a(t)^2}\right].

Preamble

import Definitions.Def_FriedmannEquations_Defs
import Mathlib

open FriedmannEquations

Formal statement

theorem FriedmannEquations.first_friedmann_dimensionless
    (G k : ℝ) (hG : 0 < G) (R ρ : ℝ → ℝ) (t t₀ : ℝ) (hR : R t ≠ 0) (hR₀ : R t₀ ≠ 0)
    (h₁ : FirstFriedmannEq G 0 k R ρ t) (h₁₀ : FirstFriedmannEq G 0 k R ρ t₀) :
    hubble (fun s => R s / R t₀) t = hubble R t ∧
    hubble (fun s => R s / R t₀) t ^ 2 =
      8 * Real.pi * G / 3 *
        (ρ t + (criticalDensity G (hubble R t₀) - ρ t₀) / (R t / R t₀) ^ 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 "Dimensionless scale factor", 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 times $t,t_0$ with $R(t)\neq0$ and $R(t_0)\ne0$ . Assume at time $t$ and at time $t_0$ (both with the same $k$ and with $\Lambda=0$ )

\Big(\frac{\dot R(s)}{R(s)}\Big)^2 = \frac{8\pi G\rho(s)}{3} - \frac{k}{R(s)^2},\qquad s\in\{t,t_0\}.

Let $a$ be the function $s\mapsto R(s)/R(t_0)$ and $H_0 = \dot R(t_0)/R(t_0)$ . Conclusion: (i) $\dot a(t)/a(t) = \dot R(t)/R(t)$ , and (ii)

\Big(\frac{\dot a(t)}{a(t)}\Big)^2 = \frac{8\pi G}{3}\left(\rho(t) + \frac{\frac{3H_0^2}{8\pi G} - \rho(t_0)}{\big(R(t)/R(t_0)\big)^2}\right).

All derivatives are deriv (junk $0$ where not differentiable); no differentiability is assumed.

View graph

First Friedmann equation in the dimensionless scale factor: H2=(a˙/a)2=8πG3[ρ+ρc−ρ0a2]H^2 = (\dot a/a)^2 = \frac{8\pi G}{3}\big[\rho + \frac{\rho_c-\rho_0}{a^2}\big]H2=(a˙/a)2=38πG​[ρ+a2ρc​−ρ0​​]

First Friedmann equation in the dimensionless scale factor: $H^2 = (\dot a/a)^2 = \frac{8\pi G}{3}\big[\rho + \frac{\rho_c-\rho_0}{a^2}\big]$