Deceleration parameter $q = -1 - \dot H/H^2$ , Eq. (31)

Proved

MDOUnifiedCosmology.deceleration_formula

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

cosmologymathematical-physics

Let $a$ be a scale factor that is differentiable at $t$ with $\dot a$ also differentiable at $t$ , and suppose $a(t)\neq0$ and $\dot a(t)\neq0$ . With $H=\dot a/a$ , the deceleration parameter satisfies

q(t)\equiv-\frac{\ddot a\,a}{\dot a^2}=-1-\frac{\dot H}{H^2}.

This is Eq. (31), used to analyse the phantom-like phase at the end of inflation and the reheating epoch.

Preamble

import Mathlib
import Definitions.Def_MDOUnifiedCosmology_model

open MDOUnifiedCosmology Set

Formal statement

namespace MDOUnifiedCosmology

theorem deceleration_formula (a : ℝ → ℝ) (t : ℝ) (ha : DifferentiableAt ℝ a t)
    (ha' : DifferentiableAt ℝ (deriv a) t) (ha0 : a t ≠ 0) (had : deriv a t ≠ 0) :
    decelerationParam a t = -1 - deriv (hubble a) t / hubble a t ^ 2 := by
  sorry

end MDOUnifiedCosmology

Source

S. H. Pereira, M. E. S. Alves, T. M. Guimarães, "An unified cosmological evolution driven by a mass dimension one fermionic field", Eur. Phys. J. C 79 (2019) 543, https://doi.org/10.1140/epjc/s10052-019-7036-5, p. 7, Eq. (31)

Human review

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

View graph

Deceleration parameter q=−1−H˙/H2q = -1 - \dot H/H^2q=−1−H˙/H2, Eq. (31)

Deceleration parameter $q = -1 - \dot H/H^2$ , Eq. (31)