Equation of state in FLRW cosmology: basic definitions

Definition

CosmologyEOS_Defs

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

cosmologymathematical-physics

Shared definitions for the mission, for real-valued functions of time $t$ : scale factor $a(t)$ , energy density $\varepsilon(t)$ , pressure $p(t)$ , Newton's constant $G$ , cosmological constant $\Lambda$ .

Equation-of-state parameter $w = p/\varepsilon$ (eosParameter p ε).
Fluid equation at time $t$ : $\dot\varepsilon(t) = -3\,\dfrac{\dot a(t)}{a(t)}\,(\varepsilon(t)+p(t))$ (FluidEquation a ε p t).
Flat Friedmann equation at time $t$ : $\left(\dfrac{\dot a(t)}{a(t)}\right)^2 = \dfrac{8\pi G}{3}\varepsilon(t)$ (FlatFriedmannEquation G a ε t).
Acceleration equation at time $t$ : $3\,\dfrac{\ddot a(t)}{a(t)} = \Lambda - 4\pi G(\varepsilon(t)+3p(t))$ (AccelerationEquation G Λ a ε p t).
Effective energy density and pressure: $\varepsilon' = \varepsilon + \dfrac{\Lambda}{8\pi G}$ , $p' = p - \dfrac{\Lambda}{8\pi G}$ .
Scalar-field equation of state: $w(\dot\phi, V) = \dfrac{\frac12\dot\phi^2 - V}{\frac12\dot\phi^2 + V}$ .

These are the objects in which every statement of the mission is phrased.

Formalization Note Derivatives are Mathlib's deriv, which returns $0$ at points of non-differentiability, so theorems assume differentiability explicitly. Divisions are total and return $0$ on a zero denominator; theorems assume nonzero denominators where it matters.

Definition code

import Mathlib

/-!
# Equation of state in FLRW cosmology — shared definitions

Source: Wikipedia, "Equation of state (cosmology)", revision 1375011367.
All quantities are real-valued; time is a real variable `t`, the scale factor is `a : ℝ → ℝ`,
the energy density is `ε : ℝ → ℝ` and the pressure is `p : ℝ → ℝ` (units with `c = 1`
in the FLRW part).
-/

namespace CosmologyEOS

open Real

/-- The equation-of-state parameter `w = p / ε` of a perfect fluid with pressure `p` and
energy density `ε`. (As a total function it returns `0` when `ε = 0`; theorems that use it
assume `ε ≠ 0`.) -/
noncomputable def eosParameter (p ε : ℝ) : ℝ := p / ε

/-- The FLRW fluid (energy-conservation) equation at time `t`:
`ε̇(t) = -3 (ȧ(t)/a(t)) (ε(t) + p(t))`. -/
def FluidEquation (a ε p : ℝ → ℝ) (t : ℝ) : Prop :=
  deriv ε t = -3 * (deriv a t / a t) * (ε t + p t)

/-- The Friedmann equation of a spatially flat FLRW universe (no cosmological constant)
at time `t`: `(ȧ(t)/a(t))² = (8πG/3) ε(t)`. -/
def FlatFriedmannEquation (G : ℝ) (a ε : ℝ → ℝ) (t : ℝ) : Prop :=
  (deriv a t / a t) ^ 2 = 8 * π * G / 3 * ε t

/-- The Friedmann acceleration equation at time `t`:
`3 ä(t)/a(t) = Λ - 4πG (ε(t) + 3 p(t))`. -/
def AccelerationEquation (G Λ : ℝ) (a ε p : ℝ → ℝ) (t : ℝ) : Prop :=
  3 * (deriv (deriv a) t / a t) = Λ - 4 * π * G * (ε t + 3 * p t)

/-- The effective energy density `ε' = ε + Λ / (8πG)`. -/
noncomputable def effectiveEnergyDensity (G Λ ε : ℝ) : ℝ := ε + Λ / (8 * π * G)

/-- The effective pressure `p' = p - Λ / (8πG)`. -/
noncomputable def effectivePressure (G Λ p : ℝ) : ℝ := p - Λ / (8 * π * G)

/-- The equation-of-state parameter of a homogeneous scalar field with time derivative
`φ̇ = phiDot` and potential energy `V`:
`w = (½ φ̇² - V) / (½ φ̇² + V)` (equal to `0` when the denominator vanishes). -/
noncomputable def scalarFieldEOS (phiDot V : ℝ) : ℝ :=
  (phiDot ^ 2 / 2 - V) / (phiDot ^ 2 / 2 + V)

end CosmologyEOS

Source

Wikipedia, "Equation of state (cosmology)", revision 1375011367, https://en.wikipedia.org/w/index.php?title=Equation_of_state_(cosmology)&oldid=1375011367, sections: lead (w = p/ε), 'FLRW equations and the equation of state', 'Scalar modeling'

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; NON-BLIND

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent that drafted the Lean statement below, with full knowledge of the source text and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; reviewers should compare the Lean code with the source themselves.

The file declares, in the namespace CosmologyEOS, the following objects (all real numbers or real functions of a real variable $t$ ).

$\mathrm{eosParameter}(p,\varepsilon) = p/\varepsilon$ , with the convention that the value is $0$ when $\varepsilon = 0$ .
$\mathrm{FluidEquation}(a,\varepsilon,p,t)$ is the proposition $\varepsilon^{\prime}(t) = -3\cdot\dfrac{a^{\prime}(t)}{a(t)}\cdot(\varepsilon(t)+p(t))$ , where $f^{\prime}(t)$ is the derivative of $f$ at $t$ if $f$ is differentiable there and $0$ otherwise, and $x/0 = 0$ .
$\mathrm{FlatFriedmannEquation}(G,a,\varepsilon,t)$ is the proposition $\left(\dfrac{a^{\prime}(t)}{a(t)}\right)^2 = \dfrac{8\pi G}{3}\,\varepsilon(t)$ (same conventions).
$\mathrm{AccelerationEquation}(G,\Lambda,a,\varepsilon,p,t)$ is the proposition $3\cdot\dfrac{a^{\prime\prime}(t)}{a(t)} = \Lambda - 4\pi G(\varepsilon(t)+3p(t))$ , where $a^{\prime\prime}$ is the derivative (same convention) of the derivative function of $a$ .
$\mathrm{effectiveEnergyDensity}(G,\Lambda,\varepsilon) = \varepsilon + \Lambda/(8\pi G)$ and $\mathrm{effectivePressure}(G,\Lambda,p) = p - \Lambda/(8\pi G)$ ; both reduce to $\varepsilon$ , resp. $p$ , when $G = 0$ (division by zero gives $0$ ).
$\mathrm{scalarFieldEOS}(\dot\phi, V) = \dfrac{\dot\phi^2/2 - V}{\dot\phi^2/2 + V}$ , equal to $0$ when $\dot\phi^2/2 + V = 0$ .

No hypotheses are attached to any of these definitions; positivity, differentiability and nonvanishing conditions must be supplied by the theorems that use them.

Human review

Endorsed by marwahaha · Oct 21, 2026

View graph