Sect. 3.1, p. 81: an expanding universe with $\rho+3p>0$ had a Big Bang

Proved

HackCosmologicalAQFT.big_bang

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

cosmologymathematical-physicsode

Let $G>0$ and let $a,\rho,p:\mathbb R\to\mathbb R$ be the scale factor, energy density and pressure. Assume:

$a$ is continuous on $\mathbb R$ ;
on the open set $\{t: a(t)>0\}$ , $a$ is twice continuously differentiable and satisfies the second Friedmann equation

\frac{\ddot a}{a}=-\frac{4\pi G}{3}(\rho+3p);

$\rho(t)+3p(t)>0$ whenever $a(t)>0$ ;
at some time $t_1$ the universe exists and expands: $a(t_1)>0$ and $\dot a(t_1)>0$ .

Then there is a finite earlier time $t_0<t_1$ at which the scale factor vanishes, a Big Bang, and the universe exists throughout $(t_0,t_1]$ :

\exists\,t_0<t_1:\qquad a(t_0)=0\quad\text{and}\quad a(t)>0\ \text{ for all } t\in(t_0,t_1].

This is the statement in Hack (2016), p. 81, that the universe "must have inevitably faced a Big Bang at some point of time in the past, i.e. there has been a $t_0>-\infty$ with $a(t_0)=0$ ". The source notes that this already follows from the second Friedmann equation together with $\dot a>0$ and $\rho+3p>0$ .

Formalization Note The scale factor is a total function on $\mathbb R$ . Only continuity is required at the Big Bang, because physical solutions such as $a(t)=t^{1/2}$ are not differentiable at $t_0$ . The source derives $\rho+3p>0$ from $\rho>0$ in the radiation era; the formal statement takes $\rho+3p>0$ (on $\{a>0\}$ ) directly as its hypothesis.

Preamble

import Mathlib
import Definitions.Def_hack_flrw_friedmann

Formal statement

namespace HackCosmologicalAQFT

/-- Hack 2016, Sect. 3.1, p. 81: occurrence of a Big Bang. -/
theorem big_bang (G : ℝ) (hG : 0 < G) (a ρ p : ℝ → ℝ)
    (ha_cont : Continuous a)
    (ha_diff : ContDiffOn ℝ 2 a {t | 0 < a t})
    (hF2 : SecondFriedmannEq G a ρ p {t | 0 < a t})
    (hSEC : ∀ t, 0 < a t → 0 < ρ t + 3 * p t)
    (t₁ : ℝ) (ha₁ : 0 < a t₁) (hexp : 0 < deriv a t₁) :
    ∃ t₀ < t₁, a t₀ = 0 ∧ ∀ t ∈ Set.Ioc t₀ t₁, 0 < a 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. 81 (first paragraph: 'there has been a

t_0>-\infty

with

a(t_0)=0

… follows already from the second Friedmann equation and the assumptions

\dot a>0

\rho>0

, since then

\rho+3p>0

and therefore

\ddot a<0

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$ and functions $a,\rho,p:\mathbb R\to\mathbb R$ . Write $U=\{t\in\mathbb R: a(t)>0\}$ . Assume:

$G>0$ ;
$a$ is continuous on all of $\mathbb R$ ;
$a$ is twice continuously differentiable on $U$ ;
for every $t\in U$ : $a''(t)/a(t)=-\frac{4\pi G}{3}\big(\rho(t)+3p(t)\big)$ , where $a'$ is the derivative of $a$ (taken as $0$ where $a$ is not differentiable) and $a''$ is the derivative of $s\mapsto a'(s)$ ;
for every $t$ with $a(t)>0$ : $\rho(t)+3p(t)>0$ ;
a real number $t_1$ with $a(t_1)>0$ and $a'(t_1)>0$ .

Conclusion. There exists a real number $t_0$ such that

$t_0<t_1$ ,
$a(t_0)=0$ , and
$a(t)>0$ for every $t$ with $t_0<t\le t_1$ .

Remarks on scope: no first Friedmann equation is assumed. No positivity of $\rho$ alone is assumed, only of $\rho+3p$ and only on $U$ . Outside $U$ the functions $a$ , $\rho$ , $p$ are unconstrained apart from continuity of $a$ ; in particular $a$ may take negative values there. $U$ is open because $a$ is continuous, and it contains $t_1$ . Nothing is asserted about times after $t_1$ or before $t_0$ .

View graph

Sect. 3.1, p. 81: an expanding universe with ρ+3p>0\rho+3p>0ρ+3p>0 had a Big Bang

Sect. 3.1, p. 81: an expanding universe with $\rho+3p>0$ had a Big Bang