Prove2Me

Acceleration equation a¨/a=−4πG3(ρ+3p)+Λ3\ddot a/a = -\frac{4\pi G}{3}(\rho+3p)+\frac{\Lambda}{3}

Proved
DarkEnergyLCDM.acceleration_equation

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

cosmologymathematical-physics

Let (a,ρr,ρm)(a, \rho_r, \rho_m) be a ΛCDM background on II with constants G,K,ΛG, K, \Lambda, and let t∈It\in I with a˙(t)≠0\dot a(t)\neq 0. Then at tt

a¨a=−4πG3(ρ+3p)+Λ3,ρ=ρr+ρm,p=ρr/3.\frac{\ddot a}{a} = -\frac{4\pi G}{3}(\rho + 3p) + \frac{\Lambda}{3},\qquad \rho = \rho_r + \rho_m,\quad p = \rho_r/3.

This is Eq. (7), the second-order equation for the scale factor.

Formalization Note The source obtains Eq. (7) from the Einstein field equations. Here it is derived from the Friedmann and continuity equations, which determine it wherever a˙≠0\dot a\neq 0. At instants with a˙=0\dot a = 0 it is not a consequence of them, so those instants are excluded.

Preamble
import Mathlib
import Definitions.Def_DarkEnergyLCDM_Defs
Formal statement
namespace DarkEnergyLCDM

theorem acceleration_equation (G K Λ : ℝ) (I : Set ℝ) (a ρr ρm : ℝ → ℝ)
    (hbg : IsLCDMBackground G K Λ I a ρr ρm) (t : ℝ) (ht : t ∈ I) (hda : deriv a t ≠ 0) :
    AccelerationEq G Λ a (fun s => ρr s + ρm s) (fun s => ρr s / 3) t := by sorry

end DarkEnergyLCDM
Source
R. von Marttens, J. Alcaniz, S. Carneiro, "A energia escura e os desafios do modelo cosmológico padrão", Cadernos de Astronomia 7(1), 62–76 (2026), https://doi.org/10.47456/Cad.Astro.v7n1.52249, p. 65, Eq. (7)

View graph