Eq. (3.7): $\rho_{\rm rad}\propto a^{-4}$ , $\rho_{\rm mat}\propto a^{-3}$ , $\rho_\Lambda$ constant

Proved

HackCosmologicalAQFT.energy_density_scaling

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

cosmologymathematical-physicsode

Let $I\subseteq\mathbb R$ be an open, connected set of cosmological times. Let $a$ be twice continuously differentiable on $I$ with $a>0$ there, and let the energy density $\rho$ be differentiable on $I$ . Suppose the pressure obeys the equation of state $p=w\rho$ on $I$ with

w\in\{\tfrac13,\ 0,\ -1\}\qquad\text{(radiation, matter, cosmological constant)},

and that the conservation law $\dot\rho+3H(\rho+p)=0$ , $H=\dot a/a$ , holds on $I$ . Then there is a constant $C\in\mathbb R$ such that

\rho(t)=C\,a(t)^{-3(1+w)}\qquad\text{for all }t\in I,

that is, $\rho\propto a^{-4}$ for radiation, $\rho\propto a^{-3}$ for matter, and $\rho$ is constant for a cosmological constant.

In Hack's normalisation, $C=\rho_0\Omega_{\rm rad}$ , $\rho_0\Omega_{\rm mat}$ , $\rho_0\Omega_\Lambda$ respectively.

Formalization Note The power $a^{-3(1+w)}$ is the real power of the positive number $a(t)$ .

Preamble

import Mathlib
import Definitions.Def_hack_flrw_friedmann

Formal statement

namespace HackCosmologicalAQFT

/-- Hack 2016, Sect. 3.1, eqs. (3.4), (3.6), (3.7): for radiation (`w = 1/3`), matter (`w = 0`)
and a cosmological constant (`w = -1`), conservation forces `ρ ∝ a^{-3(1+w)}`. -/
theorem energy_density_scaling (a ρ p : ℝ → ℝ) (w : ℝ) (hw : w = 1 / 3 ∨ w = 0 ∨ w = -1)
    (I : Set ℝ) (hI : IsOpen I) (hIc : IsPreconnected I)
    (ha : ContDiffOn ℝ 2 a I) (hpos : ∀ t ∈ I, 0 < a t)
    (hρ : DifferentiableOn ℝ ρ I) (hp : ∀ t ∈ I, p t = w * ρ t)
    (hcons : ∀ t ∈ I, deriv ρ t + 3 * hubbleRate a t * (ρ t + p t) = 0) :
    ∃ C : ℝ, ∀ t ∈ I, ρ t = C * a t ^ (-(3 * (1 + w))) := 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, pp. 79–80, eqs. (3.4), (3.6), (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 functions $a,\rho,p:\mathbb R\to\mathbb R$ , a real number $w$ , and a set $I\subseteq\mathbb R$ . Assume:

$w=\tfrac13$ or $w=0$ or $w=-1$ ;
$I$ is open and preconnected (connected or empty);
$a$ is twice continuously differentiable on $I$ and $a(t)>0$ for all $t\in I$ ;
$\rho$ is differentiable on $I$ ;
$p(t)=w\,\rho(t)$ for all $t\in I$ ;
for all $t\in I$ : $\rho'(t)+3\,\frac{a'(t)}{a(t)}\big(\rho(t)+p(t)\big)=0$ .

Conclusion. There exists a real constant $C$ (of any sign, possibly $0$ ) such that for every $t\in I$

\rho(t)=C\cdot a(t)^{-3(1+w)},

with the real power of the positive base $a(t)$ . Concretely the exponent is $-4$ for $w=\tfrac13$ , $-3$ for $w=0$ , and $0$ for $w=-1$ ; in the last case $a(t)^0=1$ and the claim is that $\rho$ is constant on $I$ . If $I$ is empty the statement holds trivially. Values of $a,\rho,p$ outside $I$ play no role.

View graph

Eq. (3.7): ρrad∝a−4\rho_{\rm rad}\propto a^{-4}ρrad​∝a−4, ρmat∝a−3\rho_{\rm mat}\propto a^{-3}ρmat​∝a−3, ρΛ\rho_\LambdaρΛ​ constant

Eq. (3.7): $\rho_{\rm rad}\propto a^{-4}$ , $\rho_{\rm mat}\propto a^{-3}$ , $\rho_\Lambda$ constant