Eq. (11): $\Lambda=(m+H)^4-m^4\sim H^4$ for $H\gg m$ and $\sim 4m^3H$ for $H\ll m$

Proved

CarneiroDeSitter.vacuumTerm_asymptotics

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

cosmologymathematical-physics

Let $m>0$ and $\Lambda(H)=(m+H)^4-m^4$ (Eq. (11)). Then

as $H\to+\infty$ , $\displaystyle \Lambda(H)\sim H^4$ , i.e. $\Lambda(H)/H^4\to1$ ;
as $H\to0^+$ , $\displaystyle \Lambda(H)\sim 4m^3H$ , i.e. $\Lambda(H)/(4m^3H)\to1$ .

These are the two regimes of the vacuum term: the cutoff-independent early-time law $\Lambda\approx H^4$ that drives the non-singular inflationary phase, and the late-time law $\Lambda\approx m^3H$ that governs the dust era.

Formalization Note $f\sim g$ is Mathlib's asymptotic equivalence Asymptotics.IsEquivalent; the second limit is taken from the right of $0$ .

Preamble

import Mathlib
import Definitions.Def_CarneiroDeSitter2006

open Real Filter Topology Asymptotics MeasureTheory Set

Formal statement

namespace CarneiroDeSitter

theorem vacuumTerm_asymptotics (m : ℝ) (hm : 0 < m) :
    (fun H => vacuumTerm m H) ~[atTop] (fun H => H ^ 4) ∧
    (fun H => vacuumTerm m H) ~[𝓝[>] 0] (fun H => 4 * m ^ 3 * H) := 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, Eq. (11) and the following paragraph

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. (11): Λ=(m+H)4−m4∼H4\Lambda=(m+H)^4-m^4\sim H^4Λ=(m+H)4−m4∼H4 for H≫mH\gg mH≫m and ∼4m3H\sim 4m^3H∼4m3H for H≪mH\ll mH≪m

Eq. (11): $\Lambda=(m+H)^4-m^4\sim H^4$ for $H\gg m$ and $\sim 4m^3H$ for $H\ll m$