Sect. 3.1, p. 80: $\rho>0$ and $\dot a>0$ once imply $a$ strictly increasing

Proved

HackCosmologicalAQFT.strictMonoOn_of_first_friedmann

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$ there, and suppose the first Friedmann equation $H^2=\frac{8\pi G}{3}\rho$ holds on $I$ with

\rho(t)>0\quad\text{for all }t\in I.

If $\dot a(t_1)>0$ at a single instant $t_1\in I$ , then $a$ is strictly increasing on all of $I$ .

This is the remark in Hack (2016), p. 80: "if $\rho>0$ for all times and $\dot a>0$ at one instant of time, then $a$ will be strictly increasing for all times." It underlies the use of $a$ and the redshift $z$ as time variables.

Preamble

import Mathlib
import Definitions.Def_hack_flrw_friedmann

Formal statement

namespace HackCosmologicalAQFT

/-- Hack 2016, Sect. 3.1, p. 80: if `ρ > 0` at all times and `ȧ > 0` at one instant, the first
Friedmann equation forces `a` to be strictly increasing at all times. -/
theorem strictMonoOn_of_first_friedmann (G : ℝ) (hG : 0 < G) (a ρ : ℝ → ℝ) (I : Set ℝ)
    (hI : IsOpen I) (hIc : IsPreconnected I)
    (ha : ContDiffOn ℝ 2 a I) (hpos : ∀ t ∈ I, 0 < a t)
    (hF1 : FirstFriedmannEq G a ρ I) (hρ : ∀ t ∈ I, 0 < ρ t)
    (t₁ : ℝ) (ht₁ : t₁ ∈ I) (hexp : 0 < deriv a t₁) :
    StrictMonoOn a I := 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 (paragraph after 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$ , and a set $I\subseteq\mathbb R$ . Assume:

$I$ is open and preconnected;
$a$ is twice continuously differentiable on $I$ , 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)$ ;
$\rho(t)>0$ for all $t\in I$ ;
there is a point $t_1\in I$ with $a'(t_1)>0$ .

Conclusion. $a$ is strictly increasing on $I$ : for all $s,t\in I$ with $s<t$ we have $a(s)<a(t)$ . Assumption 5 forces $I$ to be nonempty. No hypothesis on the second Friedmann equation or on a pressure is made.

View graph

Sect. 3.1, p. 80: ρ>0\rho>0ρ>0 and a˙>0\dot a>0a˙>0 once imply aaa strictly increasing

Sect. 3.1, p. 80: $\rho>0$ and $\dot a>0$ once imply $a$ strictly increasing