Eq. (11): $\Gamma = \tfrac32(1-\Omega_m)H$

Proved

CarneiroParticleCreation.creation_rate_eq11

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

cosmologymathematical-physicsordinary-differential-equations

Let $\Gamma, H, \rho_m, \Lambda$ be real numbers with $H\neq0$ . Assume the Friedmann equation $\rho_m+\Lambda = 3H^2$ and the vacuum law $\Lambda = 2\Gamma H$ (Eq. (10) with $\lambda_0=0$ ). Then, with $\Omega_m = \rho_m/(3H^2)$ ,

\Gamma = \frac32\,(1-\Omega_m)\,H.

In the de Sitter limit $\Omega_m=0$ this gives $\Gamma = 3H/2$ .

Preamble

import Mathlib
open Filter Topology

Formal statement

namespace CarneiroParticleCreation

theorem creation_rate_eq11 (Γ H ρm Λ : ℝ) (hH : H ≠ 0)
    (h8 : ρm + Λ = 3 * H ^ 2) (h10 : Λ = 2 * Γ * H) :
    Γ = 3 / 2 * (1 - ρm / (3 * H ^ 2)) * H := 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, Eq. (11)

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. (11): Γ=32(1−Ωm)H\Gamma = \tfrac32(1-\Omega_m)HΓ=23​(1−Ωm​)H

Eq. (11): $\Gamma = \tfrac32(1-\Omega_m)H$