p. 2245: $\Omega_m=1-H^2$ , $\Omega_\Lambda=H^2$ , $q=1-2H^2$ in the early universe

Proved

CarneiroDeSitter.early_time_density_parameters

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

cosmologymathematical-physics

Let $H,\rho_T,\rho_m,\Lambda:\mathbb R\to\mathbb R$ satisfy, for all $s$ , $\rho_T(s)=3H(s)^2$ , $\Lambda(s)=3H(s)^4$ and $\rho_T(s)=\rho_m(s)+\Lambda(s)$ . Let $t$ be a time with $H(t)\neq0$ at which $H$ solves the evolution equation (12), $\dot H(t)=-2H(t)^2+2H(t)^4$ . Then

$\Omega_m(t)=\rho_m(t)/\rho_T(t)=1-H(t)^2$ ;
$\Omega_\Lambda(t)=\Lambda(t)/\rho_T(t)=H(t)^2$ ;
the deceleration parameter $q(t)=-1-\dot H(t)/H(t)^2$ equals $1-2H(t)^2$ .

These identities describe the phase transition: as $H$ falls from $1$ to $0$ , $\Omega_m$ goes from $0$ to $1$ and $q$ from $-1$ to $1$ .

Preamble

import Mathlib
import Definitions.Def_CarneiroDeSitter2006

open Real Filter Topology Asymptotics MeasureTheory Set

Formal statement

namespace CarneiroDeSitter

theorem early_time_density_parameters (H ρT ρm Λ : ℝ → ℝ) (t : ℝ)
    (hFriedmann : ∀ s, ρT s = 3 * H s ^ 2)
    (hVacuum : ∀ s, Λ s = 3 * H s ^ 4)
    (hSplit : ∀ s, ρT s = ρm s + Λ s)
    (hode : HasDerivAt H (-2 * H t ^ 2 + 2 * H t ^ 4) t)
    (hH : H t ≠ 0) :
    ρm t / ρT t = 1 - H t ^ 2 ∧ Λ t / ρT t = H t ^ 2 ∧
    decelerationParameter H t = 1 - 2 * H t ^ 2 := by sorry

end CarneiroDeSitter

Source

S. Carneiro, "From de Sitter to de Sitter: a non-singular inflationary universe driven by vacuum", Int. J. Mod. Phys. D 15 (2006) 2241-2247, https://doi.org/10.1142/S0218271806009510, p. 2245, first paragraph (relative energy densities and deceleration factor); Figs. 2, 3

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

p. 2245: Ωm=1−H2\Omega_m=1-H^2Ωm​=1−H2, ΩΛ=H2\Omega_\Lambda=H^2ΩΛ​=H2, q=1−2H2q=1-2H^2q=1−2H2 in the early universe

p. 2245: $\Omega_m=1-H^2$ , $\Omega_\Lambda=H^2$ , $q=1-2H^2$ in the early universe