Prove2Me

Eq. (4): H˙+2H2−2H4=0\dot H + 2H^2 - 2H^4 = 0 for Λ=3H4\Lambda = 3H^4

Proved
CarneiroParticleCreation.hubble_ode_quartic_vacuum

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

cosmologymathematical-physicsordinary-differential-equations

Let I⊆RI\subseteq\mathbb R be an open set of times, and let HH, ρm\rho_m, Λ\Lambda be real functions of time with HH differentiable at every t∈It\in I. Assume that for all t∈It\in I:

  1. the vacuum law Λ(t)=3H(t)4\Lambda(t) = 3H(t)^4;
  2. the balance equation (2) with relativistic matter, ρ˙m+3H(ρm+ρm3)=−Λ˙\dot\rho_m + 3H\left(\rho_m + \tfrac{\rho_m}{3}\right) = -\dot\Lambda;
  3. the Friedmann equation (3), ρm+Λ=3H2\rho_m + \Lambda = 3H^2;
  4. H(t)≠0H(t)\neq 0.

Then for every t∈It\in I,

H˙+2H2−2H4=0.\dot H + 2H^2 - 2H^4 = 0.

This is the evolution equation of the non-singular model recalled in the introduction of the paper.

Preamble
import Mathlib
open Filter Topology
Formal statement
namespace CarneiroParticleCreation

theorem hubble_ode_quartic_vacuum (I : Set ℝ) (hI : IsOpen I) (H ρm Λ : ℝ → ℝ)
    (hH : ∀ t ∈ I, DifferentiableAt ℝ H t)
    (hΛ : ∀ t ∈ I, Λ t = 3 * H t ^ 4)
    (h2 : ∀ t ∈ I, deriv ρm t + 3 * H t * (ρm t + ρm t / 3) = - deriv Λ t)
    (h3 : ∀ t ∈ I, ρm t + Λ t = 3 * H t ^ 2)
    (hH0 : ∀ t ∈ I, H t ≠ 0) :
    ∀ t ∈ I, deriv H t + 2 * H t ^ 2 - 2 * H t ^ 4 = 0 := 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, Eqs. (2)-(4)
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