Prove2Me

Density parameters sum to one: ΩΛ+Ωm+Ωr+Ωk=1\Omega_\Lambda+\Omega_m+\Omega_r+\Omega_k=1

Proved
DarkEnergyLCDM.density_params_sum_eq_one

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

cosmologymathematical-physics

Let (a,ρr,ρm)(a, \rho_r, \rho_m) be a ΛCDM background on II with constants G,K,ΛG, K, \Lambda. Let t0∈It_0\in I with a(t0)=1a(t_0)=1 and H0=H(t0)≠0H_0 = H(t_0)\neq 0. With the density parameters of Eq. (6) evaluated at t0t_0,

ΩΛ+Ωm+Ωr+Ωk=1.\Omega_\Lambda + \Omega_m + \Omega_r + \Omega_k = 1.

This is the closure condition stated after Eq. (6).

Preamble
import Mathlib
import Definitions.Def_DarkEnergyLCDM_Defs
Formal statement
namespace DarkEnergyLCDM

theorem density_params_sum_eq_one (G K Λ : ℝ) (I : Set ℝ) (a ρr ρm : ℝ → ℝ)
    (hbg : IsLCDMBackground G K Λ I a ρr ρm) (t₀ : ℝ) (ht₀ : t₀ ∈ I) (ha₀ : a t₀ = 1)
    (hH₀ : hubble a t₀ ≠ 0) :
    lambdaParam Λ (hubble a t₀) + densityParam G (hubble a t₀) (ρm t₀)
      + densityParam G (hubble a t₀) (ρr t₀) + curvatureParam K (hubble a t₀) = 1 := 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, after Eq. (6)

View graph