No acceleration without $\Lambda$ for $\rho,p\ge0$

Proved

DarkEnergyLCDM.no_acceleration_without_lambda

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

cosmologymathematical-physics

Let $G>0$ , and let $t$ be an instant with $a(t)>0$ , $\rho(t)\ge 0$ and $p(t)\ge0$ . Suppose the acceleration equation (7) holds at $t$ with $\Lambda = 0$ . Then

\ddot a(t) \le 0.

This is the observation, made after Eq. (7), that without a cosmological constant positive acceleration is impossible because $\rho$ and $p$ are non-negative.

Preamble

import Mathlib
import Definitions.Def_DarkEnergyLCDM_Defs

Formal statement

namespace DarkEnergyLCDM

theorem no_acceleration_without_lambda (G : ℝ) (hG : 0 < G) (a ρ p : ℝ → ℝ) (t : ℝ)
    (ha : 0 < a t) (hρ : 0 ≤ ρ t) (hp : 0 ≤ p t)
    (hacc : AccelerationEq G 0 a ρ p t) :
    deriv (deriv a) t ≤ 0 := 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, text between Eqs. (7) and (8)

View graph

No acceleration without Λ\LambdaΛ for ρ,p≥0\rho,p\ge0ρ,p≥0

No acceleration without $\Lambda$ for $\rho,p\ge0$