Prove2Me

Eq. (5): the non-singular solution 2t=1/H−artanh⁡H2t = 1/H - \operatorname{artanh} H

Proved
CarneiroParticleCreation.nonsingular_solution_eq5

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

cosmologymathematical-physicsordinary-differential-equations

There is a function H:R→RH:\mathbb R\to\mathbb R such that:

  1. 0<H(t)<10 < H(t) < 1 for every tt;
  2. HH satisfies the implicit relation (5)
2t=1H(t)−artanh⁡H(t)for every t;2t = \frac{1}{H(t)} - \operatorname{artanh} H(t) \quad\text{for every } t;
  1. HH is differentiable everywhere and solves Eq. (4), H˙(t)=−2H(t)2+2H(t)4\dot H(t) = -2H(t)^2 + 2H(t)^4;
  2. H(t)→1H(t)\to 1 (the de Sitter value) as t→−∞t\to-\infty;
  3. H(t) t→12H(t)\,t \to \tfrac12 (a radiation phase) as t→+∞t\to+\infty.

Since h↦1/h−artanh⁡hh\mapsto 1/h - \operatorname{artanh} h is a bijection from (0,1)(0,1) onto R\mathbb R, item 2 determines HH uniquely. The statement therefore says that this unique function is a smooth, everywhere-defined solution of Eq. (4) with the stated asymptotics.

Preamble
import Mathlib
open Filter Topology
Formal statement
namespace CarneiroParticleCreation

theorem nonsingular_solution_eq5 :
    ∃ 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 (fun t => H t * t) atTop (𝓝 (1 / 2)) := by sorry

end CarneiroParticleCreation
Source
S. Carneiro, "Inflation driven by particle creation", AIP Conf. Proc. 1471 (2012) 61-65, https://doi.org/10.1063/1.4756813, p. 61, Eq. (5) and the following paragraph; Fig. 1
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