Eq. (12): $\dot H+2H^2-2H^4=0$ for radiation plus vacuum $\Lambda=3H^4$

Proved

CarneiroDeSitter.early_time_evolution_equation

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

cosmologymathematical-physics

Let $H,\rho_T,\rho_m,p_m,\Lambda:\mathbb R\to\mathbb R$ be the Hubble parameter, total density, matter density, matter pressure and vacuum term of a spatially flat FLRW universe, and suppose that for all times $s$

(Friedmann) $\rho_T(s)=3H(s)^2$ ;
(early-time vacuum) $\Lambda(s)=3H(s)^4$ ;
$\rho_T(s)=\rho_m(s)+\Lambda(s)$ ;
(radiation) $p_m(s)=\rho_m(s)/3$ .

Let $t$ be a time at which $H$ is differentiable, $H(t)\neq0$ , and the conservation equation (3) holds with total pressure $p_T=p_m-\Lambda$ :

\dot\rho_T(t)+3H(t)\big(\rho_T(t)+p_m(t)-\Lambda(t)\big)=0 .

Then

\dot H(t)+2H(t)^2-2H(t)^4=0 .

This is the evolution equation (12) of the early universe in Carneiro's model.

Preamble

import Mathlib
import Definitions.Def_CarneiroDeSitter2006

open Real Filter Topology Asymptotics MeasureTheory Set

Formal statement

namespace CarneiroDeSitter

theorem early_time_evolution_equation (H ρT ρm pm Λ : ℝ → ℝ) (t : ℝ)
    (hFriedmann : ∀ s, ρT s = 3 * H s ^ 2)
    (hVacuum : ∀ s, Λ s = 3 * H s ^ 4)
    (hSplit : ∀ s, ρT s = ρm s + Λ s)
    (hRadiation : ∀ s, pm s = ρm s / 3)
    (hdiff : DifferentiableAt ℝ H t)
    (hcons : deriv ρT t + 3 * H t * (ρT t + (pm t - Λ t)) = 0)
    (hH : H t ≠ 0) :
    deriv H t + 2 * H t ^ 2 - 2 * H t ^ 4 = 0 := 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. 2244, Eqs. (3), (12) and the preceding paragraph; Eq. (4) on p. 2243

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

Eq. (12): H˙+2H2−2H4=0\dot H+2H^2-2H^4=0H˙+2H2−2H4=0 for radiation plus vacuum Λ=3H4\Lambda=3H^4Λ=3H4

Eq. (12): $\dot H+2H^2-2H^4=0$ for radiation plus vacuum $\Lambda=3H^4$