Flat FLRW cosmology: Hubble rate $H=\dot a/a$ and the two Friedmann equations

Definition

hack_flrw_friedmann

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

cosmologymathematical-physics

This definition file fixes the notation of Hack (2016), Section 3.1, for spatially flat FLRW cosmology.

Let $a:\mathbb R\to\mathbb R$ be the scale factor, $\rho,p:\mathbb R\to\mathbb R$ the energy density and pressure, $G$ Newton's constant, and $I\subseteq\mathbb R$ a set of cosmological times.

Hubble rate (eq. (3.1)): $H(t)=\dfrac{\dot a(t)}{a(t)}$ .
First Friedmann equation on $I$ (eq. (3.5)): for every $t\in I$ ,

H(t)^2=\frac{8\pi G}{3}\,\rho(t).

Second Friedmann equation on $I$ (eq. (3.5)): for every $t\in I$ ,

\frac{\ddot a(t)}{a(t)}=-\frac{4\pi G}{3}\,\big(\rho(t)+3p(t)\big).

Every statement in the mission is phrased in terms of these three objects.

Formalization Note Derivatives are Mathlib's deriv (equal to $0$ where the function is not differentiable) and $\ddot a$ is the derivative of the function $t\mapsto\dot a(t)$ . Lean's division gives $x/0=0$ . The definitions impose no regularity or positivity; each theorem states these hypotheses explicitly.

Definition code

import Mathlib

namespace HackCosmologicalAQFT

/-- The Hubble rate `H(t) = ȧ(t) / a(t)` of a scale factor `a` (Hack 2016, eq. (3.1)). -/
noncomputable def hubbleRate (a : ℝ → ℝ) (t : ℝ) : ℝ := deriv a t / a t

/-- The first Friedmann equation `H² = (8πG/3) ρ` (Hack 2016, eq. (3.5)),
holding at every cosmological time `t ∈ I`. -/
def FirstFriedmannEq (G : ℝ) (a ρ : ℝ → ℝ) (I : Set ℝ) : Prop :=
  ∀ t ∈ I, hubbleRate a t ^ 2 = 8 * Real.pi * G / 3 * ρ t

/-- The second Friedmann equation `ä / a = -(4πG/3) (ρ + 3p)` (Hack 2016, eq. (3.5)),
holding at every cosmological time `t ∈ I`. -/
def SecondFriedmannEq (G : ℝ) (a ρ p : ℝ → ℝ) (I : Set ℝ) : Prop :=
  ∀ t ∈ I, deriv (deriv a) t / a t = -(4 * Real.pi * G / 3) * (ρ t + 3 * p t)

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. 78–80, eqs. (3.1), (3.5)

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.

The file introduces three objects, all for real-valued functions of a real variable $t$ .

Hubble rate. For a function $a:\mathbb R\to\mathbb R$ and $t\in\mathbb R$ , $H_a(t)$ is defined as $a'(t)/a(t)$ . Here $a'(t)$ is the derivative of $a$ at $t$ when $a$ is differentiable at $t$ , and $a'(t)=0$ otherwise. If $a(t)=0$ , the quotient is defined to be $0$ . No hypothesis on $a$ is built in.

First Friedmann equation. For a real number $G$ , functions $a,\rho:\mathbb R\to\mathbb R$ and a set $I\subseteq\mathbb R$ , the proposition holds iff for every $t\in I$

H_a(t)^2=\frac{8\pi G}{3}\,\rho(t),

with $H_a$ as above (including its conventions at non-differentiable points and at zeros of $a$ ). No sign condition on $G$ is imposed.

Second Friedmann equation. For a real number $G$ , functions $a,\rho,p:\mathbb R\to\mathbb R$ and a set $I\subseteq\mathbb R$ , the proposition holds iff for every $t\in I$

\frac{a''(t)}{a(t)}=-\frac{4\pi G}{3}\big(\rho(t)+3p(t)\big).

Here $a''(t)$ is the derivative at $t$ of the function $s\mapsto a'(s)$ , where $a'(s)$ is defined as above. It is $0$ if that function is not differentiable at $t$ , and the quotient is $0$ when $a(t)=0$ .

If $I$ is empty, both equations hold trivially.

View graph

Flat FLRW cosmology: Hubble rate H=a˙/aH=\dot a/aH=a˙/a and the two Friedmann equations

Flat FLRW cosmology: Hubble rate $H=\dot a/a$ and the two Friedmann equations