Prove2Me

Carneiro (2006): plane wave, vacuum term (m+H)4−m4(m+H)^4-m^4, dust scale factor, deceleration parameter

Definition
CarneiroDeSitter2006

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

cosmologymathematical-physics

Basic objects of S. Carneiro's decaying-vacuum cosmology (all quantities in Planck units).

  1. Wave number and damping rate (Eqs. (7)–(8)). For a frequency ω\omega and a Hubble parameter HH,
k(ω,H)=2 ω2(1+1+(3H/ω)2)1/2,b(ω,H)=32 H2(1+1+(3H/ω)2)−1/2.k(\omega,H)=\frac{\sqrt2\,\omega}{2}\Big(1+\sqrt{1+(3H/\omega)^2}\Big)^{1/2},\qquad b(\omega,H)=\frac{3\sqrt2\,H}{2}\Big(1+\sqrt{1+(3H/\omega)^2}\Big)^{-1/2}.
  1. Damped radial plane wave (Eq. (6)). For a complex amplitude ϕ0\phi_0 and real b,ω,kb,\omega,k,
ϕ(t,r)=ϕ0 e−br e−i(ωt−kr).\phi(t,r)=\phi_0\,e^{-br}\,e^{-i(\omega t-kr)} .
  1. Renormalized vacuum term (Eq. (11)). For a cutoff mm and Hubble parameter HH,
Λ(m,H)=(m+H)4−m4.\Lambda(m,H)=(m+H)^4-m^4 .
  1. Dust-phase scale factor (Eq. (14)). For constants C,σC,\sigma,
a(t)=C (eσt/2−1)2/3.a(t)=C\,\big(e^{\sigma t/2}-1\big)^{2/3}.
  1. Deceleration parameter. For a Hubble function H(t)H(t), q(t)=−1−H˙(t)/H(t)2q(t)=-1-\dot H(t)/H(t)^2, which equals −aa¨/a˙2-a\ddot a/\dot a^2 when H=a˙/aH=\dot a/a.

These definitions are shared by all statements of the mission.

Formalization Note The power 2/32/3 in item 4 is the real power function; it agrees with the intended value whenever eσt/2−1≥0e^{\sigma t/2}-1\ge 0, i.e. for σt≥0\sigma t\ge 0. Division by ω=0\omega=0 or H=0H=0 returns 00 in Lean; every theorem using items 1 or 5 assumes ω>0\omega>0 or H(t)≠0H(t)\neq 0, respectively.

Definition code
import Mathlib

/-!
# Definitions for Carneiro (2006), "From de Sitter to de Sitter"

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. All quantities are in Planck units.
-/

namespace CarneiroDeSitter

/-- Eq. (7): the wave number `k` of the radial plane-wave solution of the massless
Klein–Gordon equation in a background with Hubble parameter `H`, for frequency `ω`:
`k = (√2 ω / 2) · (1 + √(1 + (3H/ω)²))^{1/2}`. -/
noncomputable def waveNumber (ω H : ℝ) : ℝ :=
  Real.sqrt 2 * ω / 2 * Real.sqrt (1 + Real.sqrt (1 + (3 * H / ω) ^ 2))

/-- Eq. (8): the damping rate `b` (inverse depth length) of the radial plane wave:
`b = (3√2 H / 2) · (1 + √(1 + (3H/ω)²))^{-1/2}`. -/
noncomputable def dampingRate (ω H : ℝ) : ℝ :=
  3 * Real.sqrt 2 * H / 2 / Real.sqrt (1 + Real.sqrt (1 + (3 * H / ω) ^ 2))

/-- Eq. (6): the damped radial plane wave `φ(t, r) = φ₀ e^{-b r} e^{-i(ω t - k r)}`. -/
noncomputable def planeWave (φ₀ : ℂ) (b ω k : ℝ) (t r : ℝ) : ℂ :=
  φ₀ * Complex.exp (-((b * r : ℝ) : ℂ)) * Complex.exp (-Complex.I * ((ω * t - k * r : ℝ) : ℂ))

/-- Eq. (11): the renormalized vacuum term `Λ = (m + H)⁴ - m⁴` (cutoff `m`, Hubble
parameter `H`). -/
def vacuumTerm (m H : ℝ) : ℝ := (m + H) ^ 4 - m ^ 4

/-- Eq. (14): the scale factor of the late-time dust phase,
`a(t) = C (e^{σ t / 2} - 1)^{2/3}` (meaningful for `σ > 0`, `t > 0`). -/
noncomputable def dustScaleFactor (C σ t : ℝ) : ℝ :=
  C * (Real.exp (σ * t / 2) - 1) ^ ((2 : ℝ) / 3)

/-- The deceleration parameter of a flat FLRW expansion with Hubble parameter `H(t)`,
`q = -1 - Ḣ / H²` (equivalently `q = -a ä / ȧ²` when `H = ȧ / a`). -/
noncomputable def decelerationParameter (H : ℝ → ℝ) (t : ℝ) : ℝ :=
  -1 - deriv H t / H t ^ 2

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, pp. 2243-2245, Eqs. (6), (7), (8), (11), (14); deceleration factor q on p. 2245
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