Eq. (3.8): a cosmological constant gives $a(t)\propto e^{\sqrt{\Lambda/3}\,t}$

Proved

HackCosmologicalAQFT.scale_factor_cosmological_constant

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

cosmologymathematical-physicsode

Let $G>0$ and let $I\subseteq\mathbb R$ be an open, connected set of cosmological times. Let $a$ be twice continuously differentiable on $I$ with $a>0$ and $\dot a>0$ there, and suppose the first Friedmann equation $H^2=\frac{8\pi G}{3}\rho$ holds on $I$ with the energy density of a cosmological constant $\Lambda>0$ ,

\rho(t)=\rho_\Lambda=\frac{\Lambda}{8\pi G}\qquad(t\in I).

Then there is a constant $C>0$ such that

a(t)=C\,e^{\sqrt{\Lambda/3}\,t}\qquad\text{for all }t\in I.

This is the $\Lambda$ -dominated (de Sitter) solution in eq. (3.8) of Hack (2016).

Formalization Note The source leaves the relation between $\rho_\Lambda$ and $\Lambda$ implicit. The standard convention $\rho_\Lambda=\Lambda/(8\pi G)$ is the one under which eq. (3.8) has exponent $\sqrt{\Lambda/3}$ .

Preamble

import Mathlib
import Definitions.Def_hack_flrw_friedmann

Formal statement

namespace HackCosmologicalAQFT

/-- Hack 2016, Sect. 3.1, eq. (3.8): domination by a cosmological constant `Λ > 0`
(energy density `ρ_Λ = Λ / (8πG)`) gives `a(t) ∝ exp(√(Λ/3) t)`. -/
theorem scale_factor_cosmological_constant (G : ℝ) (hG : 0 < G) (a ρ : ℝ → ℝ) (I : Set ℝ)
    (hI : IsOpen I) (hIc : IsPreconnected I)
    (ha : ContDiffOn ℝ 2 a I) (hpos : ∀ t ∈ I, 0 < a t) (hexp : ∀ t ∈ I, 0 < deriv a t)
    (hF1 : FirstFriedmannEq G a ρ I)
    (Λ : ℝ) (hΛ : 0 < Λ) (hρ : ∀ t ∈ I, ρ t = Λ / (8 * Real.pi * G)) :
    ∃ C > 0, ∀ t ∈ I, a t = C * Real.exp (Real.sqrt (Λ / 3) * t) := by sorry

end HackCosmologicalAQFT

Source

T.-P. Hack, *Cosmological Applications of Algebraic Quantum Field Theory in Curved Spacetimes*, SpringerBriefs in Mathematical Physics 6, Springer, 2016, DOI 10.1007/978-3-319-21894-6 (https://doi.org/10.1007/978-3-319-21894-6), Sect. 3.1, p. 80, eq. (3.8) (with eq. (3.7))

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — non-blind, same agent as drafter

NON-BLIND READ-BACK — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source text and of the intended meaning. It was not produced by a blind, independent auditor, so it may silently read the intended meaning into the code. Reviewers must not mistake it for independent testimony; compare the Lean code against the source directly.

Fix $G\in\mathbb R$ with $G>0$ , functions $a,\rho:\mathbb R\to\mathbb R$ , a set $I\subseteq\mathbb R$ , and a real number $\Lambda$ . Assume:

$I$ is open and preconnected;
$a$ is twice continuously differentiable on $I$ ; $a(t)>0$ and $a'(t)>0$ for all $t\in I$ ;
for all $t\in I$ : $\left(a'(t)/a(t)\right)^2=\frac{8\pi G}{3}\rho(t)$ ;
$\Lambda>0$ , and $\rho(t)=\dfrac{\Lambda}{8\pi G}$ for all $t\in I$ .

Conclusion. There exists a real number $C>0$ such that for every $t\in I$

a(t)=C\,\exp\!\Big(\sqrt{\Lambda/3}\;t\Big),

where $\sqrt{\cdot}$ is the real square root (here of a positive number). The constant $C$ does not depend on $t$ . If $I$ is empty the statement holds trivially.

View graph

Eq. (3.8): a cosmological constant gives a(t)∝eΛ/3 ta(t)\propto e^{\sqrt{\Lambda/3}\,t}a(t)∝eΛ/3​t

Eq. (3.8): a cosmological constant gives $a(t)\propto e^{\sqrt{\Lambda/3}\,t}$