Deceleration parameter $q=\tfrac12\Omega_M-\Omega_\Lambda$ (eq. 29); accelerated expansion requires $\Lambda>0$

Proved

CosmoConstCentury.deceleration_parameter_and_cosmic_acceleration

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

cosmologygeneral-relativitymathematical-physics

Let $G>0$ and $c>0$ , let $\Lambda$ be the cosmological constant and $k$ a real curvature index, and let $(R,\rho)$ solve the Friedmann–Lemaître dust equations on a set of times $I$ . Let $t\in I$ , and write $H=R'/R$ , $q=-\frac{1}{H^2}\frac{R''}{R}$ , $\Omega_M=\rho/\rho_c$ with $\rho_c=3H^2/(8\pi G)$ , and $\Omega_\Lambda=\Lambda/(3H^2)$ .

If $R'(t)\neq0$ , then the deceleration parameter satisfies equation (29) of the review:

q=\frac12\,\Omega_M-\Omega_\Lambda .

If the expansion is accelerating at time $t$ , $R''(t)>0$ , and the matter density is non-negative, $\rho(t)\ge0$ , then

\Lambda>0 .

The first part generalizes (28) to cosmologies with a cosmological constant; the second part is the reason why the observed acceleration of cosmic expansion (Sections 9–10) points to a positive cosmological constant.

Formalization Note The predicate IsFriedmannSolution G c Λ k I R ρ requires, at every $t\in I$ , that $R(t)>0$ , that $R$ is $C^2$ in a neighbourhood of $t$ , and that the two equations hold with $\kappa=8\pi G/c^2$ .

Preamble

import Mathlib
import Definitions.Def_CosmoConstCentury_Defs

open Filter Topology

Formal statement

namespace CosmoConstCentury

theorem deceleration_parameter_and_cosmic_acceleration (G c Λ k : ℝ) (hG : 0 < G) (hc : 0 < c)
    (I : Set ℝ) (R ρ : ℝ → ℝ) (hsol : IsFriedmannSolution G c Λ k I R ρ) (t : ℝ) (ht : t ∈ I) :
    (deriv R t ≠ 0 → decelParam R t = omegaMatter G R ρ t / 2 - omegaLambda Λ R t) ∧
    (0 < deriv (deriv R) t → 0 ≤ ρ t → 0 < Λ) := by sorry

end CosmoConstCentury

Source

C. O'Raifeartaigh, M. O'Keeffe, W. Nahm, S. Mitton, "One hundred years of the cosmological constant: from 'superfluous stunt' to dark energy", Eur. Phys. J. H 43, 73-117 (2018), https://doi.org/10.1140/epjh/e2017-80061-7; Section 7, pp. 92-93, eq. (29) (with eqs. (25)-(28)); density parameters Section 5.1 p. 85; accelerating expansion Sections 9.1 and 10.

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Disclosure: non-blind read-back. This read-back was written by the same agent that drafted the Lean statement (Aristotle, by Harmonic), at the explicit request of the proposal owner. It is not an independent or blind audit, and it must not be treated as independent testimony: its author knew the source paper and the intended meaning while writing it. Reviewers should compare it against the Lean code themselves.

Let $G,c,\Lambda,k$ be real numbers with $G>0$ and $c>0$ ; let $I\subseteq\mathbb R$ be any set and let $R,\rho:\mathbb R\to\mathbb R$ form a Friedmann solution on $I$ : for every $s\in I$ , $R(s)>0$ , $R$ is $C^2$ near $s$ , and

\frac{3R'(s)^2}{R(s)^2}+\frac{3kc^2}{R(s)^2}-\Lambda=\kappa c^2\rho(s),\qquad \frac{R'(s)^2}{R(s)^2}+\frac{2R''(s)}{R(s)}+\frac{kc^2}{R(s)^2}-\Lambda=0,\qquad \kappa=\frac{8\pi G}{c^2}.

Let $t\in I$ . Write $H=R'(t)/R(t)$ , $q=-\dfrac{1}{H^2}\dfrac{R''(t)}{R(t)}$ , $\rho_c=\dfrac{3H^2}{8\pi G}$ , $\Omega_M=\rho(t)/\rho_c$ , $\Omega_\Lambda=\dfrac{\Lambda}{3H^2}$ . The conclusion is the conjunction of:

if $R'(t)\neq0$ , then $q=\dfrac{\Omega_M}{2}-\Omega_\Lambda$ ;
if $R''(t)>0$ and $\rho(t)\ge0$ , then $\Lambda>0$ .

Part 2 does not require $R'(t)\neq0$ . The curvature index $k$ is an arbitrary real number and does not appear in the conclusion. Only the single time $t$ is involved; $I$ may be any set containing $t$ .

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Deceleration parameter q=12ΩM−ΩΛq=\tfrac12\Omega_M-\Omega_\Lambdaq=21​ΩM​−ΩΛ​ (eq. 29); accelerated expansion requires Λ>0\Lambda>0Λ>0

Deceleration parameter $q=\tfrac12\Omega_M-\Omega_\Lambda$ (eq. 29); accelerated expansion requires $\Lambda>0$