Prove2Me

Fluid + acceleration equations give the first Friedmann equation with a constant of integration kk

Proved
FriedmannEquations.exists_curvature_of_fluidEq

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

cosmologyfriedmann-equationsgeneral-relativity

Let G,Λ∈RG,\Lambda\in\mathbb R and let II be an open, (pre)connected time interval on which the scale factor RR is positive and C2C^2 and the density ρ\rho is differentiable. Suppose that at 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. Then there is a constant k∈Rk\in\mathbb R such that the first Friedmann equation

(R˙R)2=8πGρ3−kR2+Λ3\Big(\frac{\dot R}{R}\Big)^2 = \frac{8\pi G\rho}{3} - \frac{k}{R^2} + \frac{\Lambda}{3}

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

Preamble
import Definitions.Def_FriedmannEquations_Defs
import Mathlib

open FriedmannEquations
Formal statement
theorem FriedmannEquations.exists_curvature_of_fluidEq
    (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)
    (hfluid : ∀ t ∈ I, FluidEq R ρ p t)
    (h₂ : ∀ t ∈ I, SecondFriedmannEq G Λ R ρ p t) :
    ∃ k : ℝ, ∀ t ∈ I, FirstFriedmannEq G Λ k R ρ 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.
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,ΛG,\Lambda (no sign assumption on GG), functions R,ρ,p:R→RR,\rho,p:\mathbb R\to\mathbb R and a set I⊆RI\subseteq\mathbb R. Assume: II is open and preconnected; R(t)>0R(t)>0 for all t∈It\in I; RR is twice continuously differentiable on II; ρ\rho is differentiable on II; for every t∈It\in I, ρ˙(t)=−3R˙(t)R(t)(ρ(t)+p(t))\dot\rho(t) = -3\frac{\dot R(t)}{R(t)}(\rho(t)+p(t)); and for every t∈It\in I, R¨(t)R(t)=Λ3−4πG3(ρ(t)+3p(t))\frac{\ddot R(t)}{R(t)} = \frac{\Lambda}{3} - \frac{4\pi G}{3}(\rho(t)+3p(t)). No assumption on pp.

Conclusion: there exists a real number kk (arbitrary real, not restricted to {−1,0,1}\{-1,0,1\}) such that for every t∈It\in I,

(R˙(t)R(t))2=8πGρ(t)3−kR(t)2+Λ3.\Big(\frac{\dot R(t)}{R(t)}\Big)^2 = \frac{8\pi G\rho(t)}{3} - \frac{k}{R(t)^2} + \frac{\Lambda}{3}.

If II is empty the conclusion is trivial.

View graph