Prove2Me

Eq. (10): late-time vacuum law Λ=2ΓH+λ0\Lambda = 2\Gamma H + \lambda_0

Proved
CarneiroParticleCreation.late_time_vacuum_law_eq10

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

cosmologymathematical-physicsordinary-differential-equations

Let I⊆RI\subseteq\mathbb R be an open, connected set of times, let Γ∈R\Gamma\in\mathbb R be a constant creation rate, and let H,ρm,ΛH,\rho_m,\Lambda be real functions of time with HH and ρm\rho_m differentiable on II. Assume that for all t∈It\in I:

  1. the balance equation (7), ρ˙m+3Hρm=Γρm\dot\rho_m + 3H\rho_m = \Gamma\rho_m;
  2. the Friedmann equation (8), ρm+Λ=3H2\rho_m + \Lambda = 3H^2;
  3. H(t)≠0H(t)\neq 0 and 3H(t)≠Γ3H(t)\neq\Gamma.

With total density ρ=ρm+Λ\rho=\rho_m+\Lambda and total pressure p=−Λp=-\Lambda (dust plus vacuum), the following are equivalent:

  • conservation of total energy (9), ρ˙+3H(ρ+p)=0\dot\rho + 3H(\rho+p) = 0 on II;
  • there is a constant λ0\lambda_0 with
Λ(t)=2ΓH(t)+λ0for all t∈I.\Lambda(t) = 2\Gamma H(t) + \lambda_0 \quad\text{for all } t\in I.

Formalization Note The condition 3H≠Γ3H\neq\Gamma is not stated in the paper. It is needed for the implication (10) ⇒\Rightarrow (9): if H≡Γ/3H\equiv\Gamma/3 is constant, then (7), (8) and (10) hold but (9) fails whenever Γρm≠0\Gamma\rho_m\neq0.

Preamble
import Mathlib
open Filter Topology
Formal statement
namespace CarneiroParticleCreation

theorem late_time_vacuum_law_eq10 (I : Set ℝ) (hI : IsOpen I) (hIc : IsPreconnected I)
    (Γ : ℝ) (H ρm Λ : ℝ → ℝ)
    (hH : ∀ t ∈ I, DifferentiableAt ℝ H t) (hρ : ∀ t ∈ I, DifferentiableAt ℝ ρm t)
    (h7 : ∀ t ∈ I, deriv ρm t + 3 * H t * ρm t = Γ * ρm t)
    (h8 : ∀ t ∈ I, ρm t + Λ t = 3 * H t ^ 2)
    (hH0 : ∀ t ∈ I, H t ≠ 0) (hΓ : ∀ t ∈ I, 3 * H t ≠ Γ) :
    (∀ t ∈ I, deriv (fun s => ρm s + Λ s) t + 3 * H t * ((ρm t + Λ t) + (- Λ t)) = 0) ↔
      ∃ lam₀ : ℝ, ∀ t ∈ I, Λ t = 2 * Γ * H t + lam₀ := 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. 62, Eqs. (7)-(10)
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