Eqs. (5)–(8): the damped plane wave solves $\ddot\phi+3H\dot\phi-\partial_r^2\phi=0$

Proved

CarneiroDeSitter.planeWave_solves_wave_equation

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

cosmologymathematical-physics

Let $\omega>0$ , let $H\in\mathbb R$ be a constant Hubble parameter, and let $\phi_0\in\mathbb C$ . Put $k=k(\omega,H)$ and $b=b(\omega,H)$ as in Eqs. (7)–(8),

k=\frac{\sqrt2\,\omega}{2}\Big(1+\sqrt{1+(3H/\omega)^2}\Big)^{1/2},\qquad b=\frac{3\sqrt2\,H}{2}\Big(1+\sqrt{1+(3H/\omega)^2}\Big)^{-1/2},

and $\phi(t,r)=\phi_0e^{-br}e^{-i(\omega t-kr)}$ . Then at every point $(t,r)$

\frac{\partial^2\phi}{\partial t^2}+3H\frac{\partial\phi}{\partial t}-\frac{\partial^2\phi}{\partial r^2}=0 .

This is Eq. (5) for a radial plane wave with slowly varying (here: constant) $H$ , and it shows that the amplitude decays with depth length $b^{-1}$ .

Formalization Note $H$ is a constant, as in the paper's approximation that $H$ varies slowly compared with the wave; the Laplacian of the radial plane wave is taken as $\partial_r^2$ . Derivatives are derivatives of complex-valued functions of one real variable.

Preamble

import Mathlib
import Definitions.Def_CarneiroDeSitter2006

open Real Filter Topology Asymptotics MeasureTheory Set

Formal statement

namespace CarneiroDeSitter

theorem planeWave_solves_wave_equation (ω H : ℝ) (hω : 0 < ω) (φ₀ : ℂ) (t r : ℝ) :
    let φ := planeWave φ₀ (dampingRate ω H) ω (waveNumber ω H)
    deriv (deriv (fun s => φ s r)) t + 3 * H * deriv (fun s => φ s r) t
      - deriv (deriv (fun x => φ t x)) r = 0 := by sorry

end CarneiroDeSitter

Source

S. Carneiro, "From de Sitter to de Sitter: a non-singular inflationary universe driven by vacuum", Int. J. Mod. Phys. D 15 (2006) 2241-2247, https://doi.org/10.1142/S0218271806009510, p. 2243, Eqs. (5), (6), (7), (8)

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

Eqs. (5)–(8): the damped plane wave solves ϕ¨+3Hϕ˙−∂r2ϕ=0\ddot\phi+3H\dot\phi-\partial_r^2\phi=0ϕ¨​+3Hϕ˙​−∂r2​ϕ=0

Eqs. (5)–(8): the damped plane wave solves $\ddot\phi+3H\dot\phi-\partial_r^2\phi=0$