The Friedmann equations imply the fluid equation $\dot\rho = -3H(\rho + p)$

Proved

FriedmannEquations.fluidEq_of_friedmann

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

cosmologyfriedmann-equationsgeneral-relativity

Let $G>0$ , $\Lambda, k\in\mathbb R$ , and let $I$ be an open time set on which the scale factor $R$ is positive and $C^2$ and the density $\rho$ is differentiable. If both Friedmann equations

H^2 = \frac{8\pi G\rho}{3} - \frac{k}{R^2} + \frac{\Lambda}{3},\qquad \frac{\ddot R}{R} = \frac{\Lambda}{3} - \frac{4\pi G}{3}(\rho+3p)

hold at every $t\in I$ (with $H = \dot R/R$ and the same constant $k$ ), then the fluid equation

\dot\rho = -3H(\rho + p)

holds at every $t\in I$ . Units $c=1$ .

Preamble

import Definitions.Def_FriedmannEquations_Defs
import Mathlib

open FriedmannEquations

Formal statement

theorem FriedmannEquations.fluidEq_of_friedmann
    (G Λ k : ℝ) (hG : 0 < G) (R ρ p : ℝ → ℝ) (I : Set ℝ) (hI_open : IsOpen I)
    (hR_pos : ∀ t ∈ I, 0 < R t) (hR : ContDiffOn ℝ 2 R I) (hρ : DifferentiableOn ℝ ρ I)
    (h₁ : ∀ t ∈ I, FirstFriedmannEq G Λ k R ρ t)
    (h₂ : ∀ t ∈ I, SecondFriedmannEq G Λ R ρ p t) :
    ∀ t ∈ I, FluidEq R ρ p 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), section "Equations", p. 2 (display after "Using the first equation, the second equation can be re-expressed as").

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$ with $G>0$ , functions $R,\rho,p:\mathbb R\to\mathbb R$ and a set $I\subseteq\mathbb R$ . Assume: $I$ is open; $R(t)>0$ for every $t\in I$ ; $R$ is twice continuously differentiable on $I$ ; $\rho$ is differentiable on $I$ ; for every $t\in I$ ,

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

and for every $t\in I$ ,

\frac{\ddot R(t)}{R(t)} = \frac{\Lambda}{3} - \frac{4\pi G}{3}\big(\rho(t)+3p(t)\big).

No assumption on $p$ . Conclusion: for every $t\in I$ ,

\dot\rho(t) = -3\,\frac{\dot R(t)}{R(t)}\,\big(\rho(t)+p(t)\big).

$I$ need not be connected; $k$ is one fixed real number for all $t\in I$ .

View graph

The Friedmann equations imply the fluid equation ρ˙=−3H(ρ+p)\dot\rho = -3H(\rho + p)ρ˙​=−3H(ρ+p)

The Friedmann equations imply the fluid equation $\dot\rho = -3H(\rho + p)$