Eq. (3.8): matter domination gives $a(t)\propto(t-t_0)^{2/3}$

Proved

HackCosmologicalAQFT.scale_factor_matter

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 (an expanding universe), and suppose the first Friedmann equation $H^2=\frac{8\pi G}{3}\rho$ holds on $I$ for a matter-dominated energy density

\rho(t)=\dfrac{K}{a(t)^3}\qquad(t\in I)

with a constant $K>0$ . Then there are constants $C>0$ and $t_0\in\mathbb R$ such that for every $t\in I$ , $t>t_0$ and

a(t)=C\,(t-t_0)^{2/3}.

This is the matter-dominated solution in eq. (3.8) of Hack (2016). The constant $t_0$ is the time at which the scale factor of this solution would vanish.

Formalization Note " $\propto$ " is encoded as equality with a strictly positive constant factor. The power is the real power of the positive number $t-t_0$ .

Preamble

import Mathlib
import Definitions.Def_hack_flrw_friedmann

Formal statement

namespace HackCosmologicalAQFT

/-- Hack 2016, Sect. 3.1, eq. (3.8): matter domination gives `a(t) ∝ (t - t₀)^{2/3}`. -/
theorem scale_factor_matter (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)
    (K : ℝ) (hK : 0 < K) (hρ : ∀ t ∈ I, ρ t = K / a t ^ 3) :
    ∃ C > 0, ∃ t₀ : ℝ, ∀ t ∈ I, t₀ < t ∧ a t = C * (t - t₀) ^ (2 / 3 : ℝ) := 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 constant $K$ . 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)$ ;
$K>0$ , and $\rho(t)=\dfrac{K}{a(t)^3}$ for all $t\in I$ .

Conclusion. There exist a real number $C>0$ and a real number $t_0$ such that for every $t\in I$ both $t_0<t$ and

a(t)=C\,(t-t_0)^{2/3},

where the power is the real power of the positive base $t-t_0$ . The constants $C,t_0$ do not depend on $t$ . If $I$ is empty the statement holds trivially (any $C>0$ , $t_0$ work).

View graph

Eq. (3.8): matter domination gives a(t)∝(t−t0)2/3a(t)\propto(t-t_0)^{2/3}a(t)∝(t−t0​)2/3

Eq. (3.8): matter domination gives $a(t)\propto(t-t_0)^{2/3}$