Eq. (13): every solution with $0<H<1$ satisfies $2(t-t_0)=1/H-\operatorname{artanh}H$

Proved

CarneiroDeSitter.early_time_implicit_solution

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

cosmologymathematical-physics

Let $H:\mathbb R\to\mathbb R$ satisfy $0<H(t)<1$ for all $t$ and solve the evolution equation (12),

\dot H(t)=-2H(t)^2+2H(t)^4\qquad\text{for all }t\in\mathbb R .

Then there is a constant $t_0$ (the origin of time) such that for all $t$

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

This is Eq. (13): up to the choice of time origin, the implicit relation describes every solution of (12) that stays between $0$ and the Planck value $1$ .

Formalization Note $\operatorname{artanh}$ is Mathlib's Real.artanh, which equals $\frac12\log\frac{1+x}{1-x}$ on $(-1,1)$ .

Preamble

import Mathlib
import Definitions.Def_CarneiroDeSitter2006

open Real Filter Topology Asymptotics MeasureTheory Set

Formal statement

namespace CarneiroDeSitter

theorem early_time_implicit_solution (H : ℝ → ℝ)
    (hbounds : ∀ t, 0 < H t ∧ H t < 1)
    (hode : ∀ t, HasDerivAt H (-2 * H t ^ 2 + 2 * H t ^ 4) t) :
    ∃ t₀ : ℝ, ∀ t, 2 * (t - t₀) = 1 / H t - Real.artanh (H t) := 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. (13) and the sentence introducing it

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. (13): every solution with 0<H<10<H<10<H<1 satisfies 2(t−t0)=1/H−artanh⁡H2(t-t_0)=1/H-\operatorname{artanh}H2(t−t0​)=1/H−artanhH

Eq. (13): every solution with $0<H<1$ satisfies $2(t-t_0)=1/H-\operatorname{artanh}H$