Prove2Me

The two Friedmann equations   ⟺  \iff fluid equation + acceleration equation (kk as a constant of integration)

Proved
FriedmannEquations.friedmann_pair_iff_fluid_and_acceleration

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

cosmologyfriedmann-equationsgeneral-relativity

Let G>0G > 0 and Λ∈R\Lambda\in\mathbb R, and let I⊆RI\subseteq\mathbb R be an open, (pre)connected time interval. Let RR be a scale factor that is positive and C2C^2 on II, let the density ρ\rho be differentiable on II, and let pp be any pressure function. Then the following are equivalent:

  1. there is a constant k∈Rk\in\mathbb R such that for every t∈It\in I both Friedmann equations hold:
(R˙R)2=8πGρ3−kR2+Λ3,R¨R=Λ3−4πG3(ρ+3p);\Big(\frac{\dot R}{R}\Big)^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);
  1. for every t∈It\in I the fluid equation ρ˙=−3R˙R(ρ+p)\dot\rho = -3\frac{\dot R}{R}(\rho+p) and the acceleration equation R¨R=Λ3−4πG3(ρ+3p)\frac{\ddot R}{R} = \frac{\Lambda}{3} - \frac{4\pi G}{3}(\rho+3p) hold.

This is the statement of the section Interpretation: "The pair of equations given above is equivalent to the following pair of equations … with kk, the spatial curvature index, serving as a constant of integration for the first equation." Units c=1c = 1 (so κc4=8πG\kappa c^4 = 8\pi G).

Preamble
import Definitions.Def_FriedmannEquations_Defs
import Mathlib

open FriedmannEquations
Formal statement
theorem FriedmannEquations.friedmann_pair_iff_fluid_and_acceleration
    (G Λ : ℝ) (hG : 0 < G) (R ρ p : ℝ → ℝ) (I : Set ℝ)
    (hI_open : IsOpen I) (hI_conn : IsPreconnected I)
    (hR_pos : ∀ t ∈ I, 0 < R t) (hR : ContDiffOn ℝ 2 R I) (hρ : DifferentiableOn ℝ ρ I) :
    (∃ k : ℝ, ∀ t ∈ I, FirstFriedmannEq G Λ k R ρ t ∧ SecondFriedmannEq G Λ R ρ p t) ↔
      (∀ t ∈ I, FluidEq R ρ p t ∧ SecondFriedmannEq G Λ 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 "Interpretation" (p. 6), together with the equations of section "FLRW models" (pp. 5–6) and "Equations" (p. 2); units c=1c=1.
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 real numbers GG and Λ\Lambda with G>0G>0, functions R,ρ,p:R→RR,\rho,p:\mathbb R\to\mathbb R, and a set I⊆RI\subseteq\mathbb R. Assume: II is open; II is preconnected (so II is an open interval, possibly empty or all of R\mathbb R); R(t)>0R(t)>0 for all t∈It\in I; RR is twice continuously differentiable on II (ContDiffOn ℝ 2); ρ\rho is differentiable on II. No assumption is made on pp.

Conclusion: the following two statements are equivalent.

(A) There exists a real number kk such that for every t∈It\in I,

(R˙(t)R(t))2=8πGρ(t)3−kR(t)2+Λ3andR¨(t)R(t)=Λ3−4πG3(ρ(t)+3p(t)).\Big(\frac{\dot R(t)}{R(t)}\Big)^2 = \frac{8\pi G\rho(t)}{3} - \frac{k}{R(t)^2} + \frac{\Lambda}{3}\quad\text{and}\quad \frac{\ddot R(t)}{R(t)} = \frac{\Lambda}{3} - \frac{4\pi G}{3}\big(\rho(t)+3p(t)\big).

(B) For every t∈It\in I,

ρ˙(t)=−3 R˙(t)R(t) (ρ(t)+p(t))andR¨(t)R(t)=Λ3−4πG3(ρ(t)+3p(t)).\dot\rho(t) = -3\,\frac{\dot R(t)}{R(t)}\,\big(\rho(t)+p(t)\big)\quad\text{and}\quad \frac{\ddot R(t)}{R(t)} = \frac{\Lambda}{3} - \frac{4\pi G}{3}\big(\rho(t)+3p(t)\big).

Here R˙,R¨,ρ˙\dot R,\ddot R,\dot\rho are the ordinary derivatives (they exist on II by the hypotheses since II is open). kk ranges over all reals, not only {−1,0,1}\{-1,0,1\}. If I=∅I=\varnothing both sides hold trivially.

View graph