Eq. (14): $a=C(e^{\sigma t/2}-1)^{2/3}$ solves the dust phase with $\Lambda=\sigma H$

Proved

CarneiroDeSitter.dust_phase_solution

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

cosmologymathematical-physics

Let $C>0$ , $\sigma>0$ , let $a(t)=C(e^{\sigma t/2}-1)^{2/3}$ be the scale factor (14), and let $H=\dot a/a$ be its Hubble parameter. With the Friedmann equation $\rho_T=3H^2$ , the late-time vacuum term $\Lambda=\sigma H$ and dust ( $p_m=0$ , so $p_T=-\Lambda$ ), the conservation equation (3) holds at every time $t>0$ :

\frac{d}{dt}\big(3H^2\big)+3H\big(3H^2-\sigma H\big)=0 .

So (14) is a solution of the late-time dust era of the model, with $C$ an integration constant.

Preamble

import Mathlib
import Definitions.Def_CarneiroDeSitter2006

open Real Filter Topology Asymptotics MeasureTheory Set

Formal statement

namespace CarneiroDeSitter

theorem dust_phase_solution (C σ : ℝ) (hC : 0 < C) (hσ : 0 < σ) (t : ℝ) (ht : 0 < t) :
    let H := fun s => deriv (dustScaleFactor C σ) s / dustScaleFactor C σ s
    deriv (fun s => 3 * H s ^ 2) t + 3 * H t * (3 * H t ^ 2 + (0 - σ * H t)) = 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. 2245, Eq. (14) and the preceding sentences

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. (14): a=C(eσt/2−1)2/3a=C(e^{\sigma t/2}-1)^{2/3}a=C(eσt/2−1)2/3 solves the dust phase with Λ=σH\Lambda=\sigma HΛ=σH

Eq. (14): $a=C(e^{\sigma t/2}-1)^{2/3}$ solves the dust phase with $\Lambda=\sigma H$