Prove2Me

p. 2245–2246: the dust solution starts as a∝t2/3a\propto t^{2/3} and tends to de Sitter with H→σ/3H\to\sigma/3

Proved
CarneiroDeSitter.dust_phase_asymptotics

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

cosmologymathematical-physics

Let C>0C>0, σ>0\sigma>0 and a(t)=C(eσt/2−1)2/3a(t)=C(e^{\sigma t/2}-1)^{2/3} (Eq. (14)). Then

  1. (Einstein–de Sitter start) as t→0+t\to0^+,
a(t)∼C(σ2)2/3t2/3;a(t)\sim C\Big(\frac\sigma2\Big)^{2/3}t^{2/3};
  1. (de Sitter end) the Hubble parameter H=a˙/aH=\dot a/a satisfies
lim⁡t→∞H(t)=σ3,\lim_{t\to\infty}H(t)=\frac\sigma3 ,

the value fixed by 3H2=Λ=σH3H^2=\Lambda=\sigma H.

Formalization Note ∼\sim is Asymptotics.IsEquivalent along t→0+t\to0^+, and t2/3t^{2/3} is the real power function.

Preamble
import Mathlib
import Definitions.Def_CarneiroDeSitter2006

open Real Filter Topology Asymptotics MeasureTheory Set
Formal statement
namespace CarneiroDeSitter

theorem dust_phase_asymptotics (C σ : ℝ) (hC : 0 < C) (hσ : 0 < σ) :
    dustScaleFactor C σ ~[𝓝[>] 0] (fun t => C * (σ / 2) ^ ((2 : ℝ) / 3) * t ^ ((2 : ℝ) / 3)) ∧
    Tendsto (fun t => deriv (dustScaleFactor C σ) t / dustScaleFactor C σ t) atTop
      (𝓝 (σ / 3)) := 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 (paragraph after Eq. (14)) and p. 2246 (de Sitter limit)
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