Matter-only deceleration (eqs. 25–28): $R''/R=-\tfrac{4\pi G}{3}\rho$ and $q=\tfrac{4\pi G}{3H^2}\rho=\tfrac12\Omega_M$

Proved

CosmoConstCentury.matter_only_deceleration

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

cosmologygeneral-relativitymathematical-physics

Let $G>0$ , $c>0$ , let $k$ be a real curvature index, and let $(R,\rho)$ solve the Friedmann–Lemaître dust equations without cosmological constant ( $\Lambda=0$ ) on a set of times $I$ . Then at every $t\in I$ :

the expansion decelerates according to (25),

\frac{R''}{R}=-\frac{4\pi G}{3}\rho;

if moreover $R'(t)\neq0$ , the deceleration parameter $q=-\frac{1}{H^2}\frac{R''}{R}$ of (26) satisfies (27) and (28),

q=\frac{4\pi G}{3H^2}\rho=\frac12\,\Omega_M .

This is the basis, recalled in Section 7, of the 1950s programme to determine the density of matter from a measurement of the deceleration parameter $q_0$ .

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 matter_only_deceleration (G c k : ℝ) (hG : 0 < G) (hc : 0 < c) (I : Set ℝ)
    (R ρ : ℝ → ℝ) (hsol : IsFriedmannSolution G c 0 k I R ρ) (t : ℝ) (ht : t ∈ I) :
    deriv (deriv R) t / R t = -(4 * Real.pi * G / 3) * ρ t ∧
    (deriv R t ≠ 0 →
      decelParam R t = 4 * Real.pi * G / (3 * hubbleParam R t ^ 2) * ρ t ∧
      decelParam R t = omegaMatter G R ρ t / 2) := 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, p. 92, eqs. (25), (26), (27), (28).

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,k$ be real numbers with $G>0$ , $c>0$ ; let $I\subseteq\mathbb R$ be any set and $R,\rho$ a Friedmann solution with $\Lambda=0$ and curvature index $k$ on $I$ (for every $s\in I$ : $R(s)>0$ , $R$ is $C^2$ near $s$ , $\dfrac{3R'(s)^2}{R(s)^2}+\dfrac{3kc^2}{R(s)^2}=\kappa c^2\rho(s)$ , $\dfrac{R'(s)^2}{R(s)^2}+\dfrac{2R''(s)}{R(s)}+\dfrac{kc^2}{R(s)^2}=0$ , $\kappa=8\pi G/c^2$ ). Let $t\in I$ . Then:

$\dfrac{R''(t)}{R(t)}=-\dfrac{4\pi G}{3}\rho(t)$ ;
if $R'(t)\neq0$ , then with $H=R'(t)/R(t)$ and $q=-\dfrac{1}{H^2}\dfrac{R''(t)}{R(t)}$ :

q=\frac{4\pi G}{3H^2}\rho(t)\qquad\text{and}\qquad q=\frac12\,\Omega_M,\quad \Omega_M=\rho(t)\Big/\frac{3H^2}{8\pi G}.

No sign of $\rho$ is assumed; $k$ is any real number.

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

Matter-only deceleration (eqs. 25–28): R′′/R=−4πG3ρR''/R=-\tfrac{4\pi G}{3}\rhoR′′/R=−34πG​ρ and q=4πG3H2ρ=12ΩMq=\tfrac{4\pi G}{3H^2}\rho=\tfrac12\Omega_Mq=3H24πG​ρ=21​ΩM​

Matter-only deceleration (eqs. 25–28): $R''/R=-\tfrac{4\pi G}{3}\rho$ and $q=\tfrac{4\pi G}{3H^2}\rho=\tfrac12\Omega_M$