From de Sitter to de Sitter: a non-singular eternal solution of $\dot H+2H^2-2H^4=0$

Proved

CarneiroDeSitter.nonsingular_de_sitter_to_de_sitter

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

cosmologymathematical-physics

There is a function $H:\mathbb R\to\mathbb R$ (the Hubble parameter, in Planck units) such that

$0<H(t)<1$ for every $t\in\mathbb R$ ;
$H$ satisfies the implicit relation (13) for every $t$ :

2t=\frac1{H(t)}-\operatorname{artanh}H(t);

$H$ is differentiable everywhere and solves the evolution equation (12):

\dot H(t)+2H(t)^2-2H(t)^4=0\qquad(t\in\mathbb R);

$H(t)\to1$ as $t\to-\infty$ (quasi-de Sitter phase at the Planck value);
$H(t)\to0$ as $t\to+\infty$ .

This is the central claim of the paper: with radiation and the early-time vacuum term $\Lambda=3H^4$ , the universe has no initial singularity, exists for an infinite past in an inflationary quasi-de Sitter state with $H\approx1$ , and undergoes a transition in which $H$ (and $\Lambda$ ) fall towards zero.

Formalization Note $\operatorname{artanh}$ is Mathlib's Real.artanh. The solution is required on the whole real line, which is what "no initial singularity, existing since an infinite past" asserts.

Preamble

import Mathlib
import Definitions.Def_CarneiroDeSitter2006

open Real Filter Topology Asymptotics MeasureTheory Set

Formal statement

namespace CarneiroDeSitter

theorem nonsingular_de_sitter_to_de_sitter :
    ∃ H : ℝ → ℝ,
      (∀ t, 0 < H t ∧ H t < 1) ∧
      (∀ t, 2 * t = 1 / H t - Real.artanh (H t)) ∧
      (∀ t, HasDerivAt H (-2 * H t ^ 2 + 2 * H t ^ 4) t) ∧
      Tendsto H atBot (𝓝 1) ∧
      Tendsto H atTop (𝓝 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. (12), (13) and the paragraph after (13); Fig. 1; abstract

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

From de Sitter to de Sitter: a non-singular eternal solution of H˙+2H2−2H4=0\dot H+2H^2-2H^4=0H˙+2H2−2H4=0

From de Sitter to de Sitter: a non-singular eternal solution of $\dot H+2H^2-2H^4=0$