Prove2Me

Eq. (16): early-time vacuum law Λ=3γ4H2+Λ0\Lambda = \tfrac{3\gamma}{4}H^2 + \Lambda_0

Proved
CarneiroParticleCreation.early_time_vacuum_law_eq16

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 γ≠4\gamma\neq4 be a constant, 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 (13) for relativistic matter, ρ˙m+3H(ρm+ρm3)=γHρm\dot\rho_m + 3H\left(\rho_m+\tfrac{\rho_m}{3}\right) = \gamma H\rho_m;
  2. the Friedmann equation (14), ρm+Λ=3H2\rho_m+\Lambda=3H^2;
  3. H(t)≠0H(t)\neq0.

With ρ=ρm+Λ\rho=\rho_m+\Lambda and p=ρm/3−Λp=\rho_m/3-\Lambda, the following are equivalent:

  • conservation of total energy (15), ρ˙+3H(ρ+p)=0\dot\rho+3H(\rho+p)=0 on II;
  • there is a constant Λ0\Lambda_0 with
Λ(t)=3γ4H(t)2+Λ0for all t∈I.\Lambda(t) = \frac{3\gamma}{4}H(t)^2 + \Lambda_0\quad\text{for all } t\in I.
Preamble
import Mathlib
open Filter Topology
Formal statement
namespace CarneiroParticleCreation

theorem early_time_vacuum_law_eq16 (I : Set ℝ) (hI : IsOpen I) (hIc : IsPreconnected I)
    (γ : ℝ) (hγ : γ ≠ 4) (H ρm Λ : ℝ → ℝ)
    (hH : ∀ t ∈ I, DifferentiableAt ℝ H t) (hρ : ∀ t ∈ I, DifferentiableAt ℝ ρm t)
    (h13 : ∀ t ∈ I, deriv ρm t + 3 * H t * (ρm t + ρm t / 3) = γ * H t * ρm t)
    (h14 : ∀ t ∈ I, ρm t + Λ t = 3 * H t ^ 2)
    (hH0 : ∀ t ∈ I, H t ≠ 0) :
    (∀ t ∈ I, deriv (fun s => ρm s + Λ s) t +
        3 * H t * ((ρm t + Λ t) + (ρm t / 3 - Λ t)) = 0) ↔
      ∃ Λ₀ : ℝ, ∀ t ∈ I, Λ t = 3 * γ / 4 * H t ^ 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. 63, Eqs. (13)-(16)
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