Prove2Me

Density scaling ρ∝a−3(1+w)\rho \propto a^{-3(1+w)} from the fluid equation with p=wρp = w\rho

Proved
FriedmannEquations.density_scaling_of_fluidEq

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

cosmologyfriedmann-equationsgeneral-relativity

Let w∈Rw\in\mathbb R and let II be an open, (pre)connected time interval on which the scale factor aa is positive and differentiable and the density ρ\rho is differentiable. If the fluid equation with equation of state p=wρp = w\rho,

ρ˙=−3H(ρ+wρ),H=a˙/a,\dot\rho = -3H(\rho + w\rho),\qquad H = \dot a/a,

holds at every t∈It\in I, then there is a constant CC with

ρ(t)=C a(t)−3(1+w)for all t∈I.\rho(t) = C\,a(t)^{-3(1+w)}\qquad\text{for all } t\in I.
Preamble
import Definitions.Def_FriedmannEquations_Defs
import Mathlib

open FriedmannEquations
Formal statement
theorem FriedmannEquations.density_scaling_of_fluidEq
    (w : ℝ) (R ρ : ℝ → ℝ) (I : Set ℝ) (hI_open : IsOpen I) (hI_conn : IsPreconnected I)
    (hR_pos : ∀ t ∈ I, 0 < R t) (hR : DifferentiableOn ℝ R I) (hρ : DifferentiableOn ℝ ρ I)
    (hfluid : ∀ t ∈ I, FluidEq R ρ (fun s => w * ρ s) t) :
    ∃ C : ℝ, ∀ t ∈ I, ρ t = C * R t ^ (-3 * (1 + w)) := 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 "Mixtures", pp. 8–9.
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 w∈Rw\in\mathbb R, functions R,ρ:R→RR,\rho:\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 and ρ\rho are differentiable on II; for every t∈It\in I,

ρ˙(t)=−3 R˙(t)R(t) (ρ(t)+wρ(t)).\dot\rho(t) = -3\,\frac{\dot R(t)}{R(t)}\,\big(\rho(t) + w\rho(t)\big).

Conclusion: there is a real CC such that for every t∈It\in I, ρ(t)=C⋅R(t)−3(1+w)\rho(t) = C\cdot R(t)^{-3(1+w)} (real power of the positive number R(t)R(t)).

View graph