Matter density scales as $a^{-3}$

Proved

DarkEnergyLCDM.matter_density_scaling

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

cosmologymathematical-physics

Let $I$ be an open connected interval, and let $a$ and $\rho$ be differentiable on $I$ with $a>0$ there. Suppose $\rho$ satisfies the continuity equation for pressureless matter ( $p = 0$ ):

\dot\rho + 3H\rho = 0 \quad\text{on } I.

If $t_0\in I$ and $a(t_0)=1$ , then $\rho(t) = \rho(t_0)\,a(t)^{-3}$ for all $t\in I$ .

This is the second half of Eq. (4): pressureless matter dilutes with the volume, as $a^{-3}$ .

Preamble

import Mathlib
import Definitions.Def_DarkEnergyLCDM_Defs

Formal statement

namespace DarkEnergyLCDM

theorem matter_density_scaling (I : Set ℝ) (hI : IsOpen I) (hIc : IsPreconnected I)
    (a ρ : ℝ → ℝ) (ha : DifferentiableOn ℝ a I) (ha_pos : ∀ t ∈ I, 0 < a t)
    (hρ : DifferentiableOn ℝ ρ I)
    (hcont : ∀ t ∈ I, ContinuityEq a ρ (fun _ => 0) t)
    (t₀ : ℝ) (ht₀ : t₀ ∈ I) (ha₀ : a t₀ = 1) :
    ∀ t ∈ I, ρ t = ρ t₀ * (a t)⁻¹ ^ 3 := by sorry

end DarkEnergyLCDM

Source

R. von Marttens, J. Alcaniz, S. Carneiro, "A energia escura e os desafios do modelo cosmológico padrão", Cadernos de Astronomia 7(1), 62–76 (2026), https://doi.org/10.47456/Cad.Astro.v7n1.52249, p. 65, Eq. (4) (matter,

w_m = 0

)

View graph

Matter density scales as a−3a^{-3}a−3

Matter density scales as $a^{-3}$