Eq. (3.6): the Friedmann equations imply $\dot\rho+3H(\rho+p)=0$

Proved

HackCosmologicalAQFT.continuity_eq_of_friedmann

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

cosmologymathematical-physicsode

Let $G>0$ , let $I\subseteq\mathbb R$ be an open set of cosmological times, and let $a,\rho,p:\mathbb R\to\mathbb R$ be the scale factor, energy density and pressure. Assume $a$ is twice continuously differentiable on $I$ with $a>0$ there, and that both Friedmann equations hold on $I$ :

H^2=\frac{8\pi G}{3}\rho,\qquad \frac{\ddot a}{a}=-\frac{4\pi G}{3}(\rho+3p),\qquad H=\frac{\dot a}{a}.

Then for every $t\in I$ the energy density obeys the conservation law

\dot\rho(t)+3H(t)\big(\rho(t)+p(t)\big)=0.

This is the observation in Hack (2016), p. 80, that eq. (3.6), the FLRW form of $\nabla^\mu T_{\mu\nu}=0$ , can be obtained directly from the Friedmann equations.

Formalization Note No differentiability of $\rho$ is assumed. On $I$ the first Friedmann equation determines $\rho$ from $a$ , so $\dot\rho$ is meaningful.

Preamble

import Mathlib
import Definitions.Def_hack_flrw_friedmann

Formal statement

namespace HackCosmologicalAQFT

/-- Hack 2016, Sect. 3.1, eq. (3.6): the Friedmann equations imply `ρ̇ + 3H(ρ + p) = 0`. -/
theorem continuity_eq_of_friedmann (G : ℝ) (hG : 0 < G) (a ρ p : ℝ → ℝ) (I : Set ℝ)
    (hI : IsOpen I) (ha : ContDiffOn ℝ 2 a I) (hpos : ∀ t ∈ I, 0 < a t)
    (hF1 : FirstFriedmannEq G a ρ I) (hF2 : SecondFriedmannEq G a ρ p I) :
    ∀ t ∈ I, deriv ρ t + 3 * hubbleRate a t * (ρ t + p t) = 0 := 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, eqs. (3.5)–(3.6)

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 a real number $G$ with $G>0$ , three functions $a,\rho,p:\mathbb R\to\mathbb R$ , and a set $I\subseteq\mathbb R$ . Assume:

$I$ is open;
$a$ is twice continuously differentiable on $I$ ;
$a(t)>0$ for every $t\in I$ ;
for every $t\in I$ : $\left(a'(t)/a(t)\right)^2=\frac{8\pi G}{3}\rho(t)$ ;
for every $t\in I$ : $a''(t)/a(t)=-\frac{4\pi G}{3}\big(\rho(t)+3p(t)\big)$ , where $a''$ is the derivative of the function $s\mapsto a'(s)$ .

Here $a'(s)$ is the derivative of $a$ at $s$ (taken as $0$ where $a$ is not differentiable). On the open set $I$ , assumption 2 makes $a'$ and $a''$ the genuine derivatives.

Conclusion. For every $t\in I$ ,

\rho'(t)+3\,\frac{a'(t)}{a(t)}\,\big(\rho(t)+p(t)\big)=0,

where $\rho'(t)$ is the derivative of $\rho$ at $t$ if $\rho$ is differentiable there, and $0$ otherwise. No hypothesis on differentiability of $\rho$ or $p$ , or on the signs of $\rho,p$ , is made. If $I$ is empty the statement holds trivially.

View graph

Eq. (3.6): the Friedmann equations imply ρ˙+3H(ρ+p)=0\dot\rho+3H(\rho+p)=0ρ˙​+3H(ρ+p)=0

Eq. (3.6): the Friedmann equations imply $\dot\rho+3H(\rho+p)=0$