Friedman's first integral (eq. 17) and conservation of $\kappa\rho R^3/3$

Proved

CosmoConstCentury.friedman_first_integral

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

cosmologygeneral-relativitymathematical-physics

Let $c>0$ , let $G$ and $\Lambda$ be real constants, and let $I\subseteq\mathbb R$ be an interval (a preconnected set of times). Let $(R,\rho)$ solve the closed ( $k=1$ ) Friedmann–Lemaître dust equations (15)–(16) on $I$ . Then there is a constant $A$ such that for every $t\in I$ :

$\dfrac{\kappa\,\rho(t)\,R(t)^3}{3}=A$ (conservation of mass), and
Friedman's relation (17) holds:

\frac{1}{c^2}\Big(\frac{dR}{dt}\Big)^2=\frac{A-R+\frac{\Lambda}{3c^2}R^3}{R}.

Friedman used this integral to show that the magnitude of $\Lambda$ decides whether a matter-filled universe expands monotonically or expands and then contracts.

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 friedman_first_integral (G c Λ : ℝ) (hc : 0 < c) (I : Set ℝ) (hI : IsPreconnected I)
    (R ρ : ℝ → ℝ) (hsol : IsFriedmannSolution G c Λ 1 I R ρ) :
    ∃ A : ℝ, ∀ t ∈ I, einsteinKappa G c * ρ t * R t ^ 3 / 3 = A ∧
      (1 / c ^ 2) * deriv R t ^ 2 = (A - R t + Λ * R t ^ 3 / (3 * c ^ 2)) / 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 4, p. 82, eqs. (15), (16), (17) (Friedman 1922).

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,\Lambda$ be real numbers with $c>0$ ; let $I\subseteq\mathbb R$ be preconnected (an interval, possibly empty, a single point, or unbounded); let $R,\rho:\mathbb R\to\mathbb R$ form a Friedmann solution with $k=1$ on $I$ : for every $t\in I$ , $R(t)>0$ , $R$ is $C^2$ near $t$ , $\dfrac{3R'(t)^2}{R(t)^2}+\dfrac{3c^2}{R(t)^2}-\Lambda=\kappa c^2\rho(t)$ and $\dfrac{R'(t)^2}{R(t)^2}+\dfrac{2R''(t)}{R(t)}+\dfrac{c^2}{R(t)^2}-\Lambda=0$ , where $\kappa=8\pi G/c^2$ .

Conclusion: there is a single real number $A$ such that for every $t\in I$ ,

\frac{\kappa\,\rho(t)\,R(t)^3}{3}=A\qquad\text{and}\qquad \frac{1}{c^2}R'(t)^2=\frac{A-R(t)+\dfrac{\Lambda R(t)^3}{3c^2}}{R(t)}.

No sign of $G$ , $\Lambda$ or $\rho$ is assumed; $A$ may be zero or negative.

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

Friedman's first integral (eq. 17) and conservation of κρR3/3\kappa\rho R^3/3κρR3/3

Friedman's first integral (eq. 17) and conservation of $\kappa\rho R^3/3$