Flat power-law solution $a(t) = a_0\,t^{2/(3(w+1))}$ for $p = w\rho$

Proved

FriedmannEquations.flat_power_law_solution

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

cosmologyfriedmann-equationsgeneral-relativity

Let $G>0$ , $w\neq -1$ and $a_0>0$ , and set $\alpha = \frac{2}{3(w+1)}$ . The scale factor $a(t) = a_0\,t^{\alpha}$ together with the density

\rho(t) = \frac{1}{6\pi G(1+w)^2 t^2}

and pressure $p = w\rho$ satisfies, at every $t>0$ , both Friedmann equations with $k = 0$ and $\Lambda = 0$ :

\Big(\frac{\dot a}{a}\Big)^2 = \frac{8\pi G\rho}{3},\qquad \frac{\ddot a}{a} = -\frac{4\pi G}{3}(\rho+3p).

(The density is the one forced by the first equation, $\rho = 3H^2/8\pi G$ with $H = \alpha/t$ .) The special cases $w=0$ ( $a\propto t^{2/3}$ , matter) and $w=1/3$ ( $a\propto t^{1/2}$ , radiation) are the source's examples.

Preamble

import Definitions.Def_FriedmannEquations_Defs
import Mathlib

open FriedmannEquations

Formal statement

theorem FriedmannEquations.flat_power_law_solution
    (G w a₀ : ℝ) (hG : 0 < G) (hw : w ≠ -1) (ha₀ : 0 < a₀) :
    let R : ℝ → ℝ := fun t => a₀ * t ^ (2 / (3 * (w + 1)))
    let ρ : ℝ → ℝ := fun t => 1 / (6 * Real.pi * G * (1 + w) ^ 2 * t ^ 2)
    ∀ t : ℝ, 0 < t →
      FirstFriedmannEq G 0 0 R ρ t ∧ SecondFriedmannEq G 0 R ρ (fun s => w * ρ s) 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 "Useful solutions", p. 8.

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,w,a_0$ with $G>0$ , $w\neq-1$ , $a_0>0$ . Define $R(t) = a_0\,t^{2/(3(w+1))}$ (real power rpow; only used at $t>0$ ) and $\rho(t) = \dfrac{1}{6\pi G(1+w)^2t^2}$ , and pressure $p(s) = w\,\rho(s)$ . Conclusion: for every real $t>0$ ,

\Big(\frac{\dot R(t)}{R(t)}\Big)^2 = \frac{8\pi G\rho(t)}{3} - \frac{0}{R(t)^2} + \frac{0}{3}\quad\text{and}\quad \frac{\ddot R(t)}{R(t)} = \frac{0}{3} - \frac{4\pi G}{3}\big(\rho(t) + 3w\rho(t)\big),

where $\dot R,\ddot R$ are the derivatives of these specific functions of $t$ (as functions on all of $\mathbb R$ , evaluated at $t>0$ ). Values $w<-1$ are included.

View graph

Flat power-law solution a(t)=a0 t2/(3(w+1))a(t) = a_0\,t^{2/(3(w+1))}a(t)=a0​t2/(3(w+1)) for p=wρp = w\rhop=wρ

Flat power-law solution $a(t) = a_0\,t^{2/(3(w+1))}$ for $p = w\rho$