Prove2Me

CPL diverges as a→∞a\to\infty for wa>0w_a>0; BA stays bounded

Proved
DarkEnergyLCDM.cpl_ba_behaviour

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

cosmologymathematical-physics

Let w0,wa∈Rw_0, w_a\in\mathbb R.

  1. If wa>0w_a>0, the CPL equation of state w(a)=w0+(1−a)waw(a) = w_0 + (1-a)w_a (Eq. 19) tends to −∞-\infty as a→∞a\to\infty.
  2. The BA equation of state w(a)=w0+wa1−aa2+(1−a)2w(a) = w_0 + w_a\frac{1-a}{a^2+(1-a)^2} (Eq. 20) is bounded for all a>0a>0: there is MM with ∣w(a)∣≤M|w(a)|\le M for every a>0a>0.

This is the comparison after Eq. (20): CPL diverges as the scale factor tends to infinity (for wa>0w_a>0), whereas BA remains well behaved at all times.

Formalization Note The source describes the CPL divergence as "exponential". The formal statement records only that the CPL equation of state is unbounded (it tends to −∞-\infty).

Preamble
import Mathlib
import Definitions.Def_DarkEnergyLCDM_Defs
Formal statement
namespace DarkEnergyLCDM

open Filter

theorem cpl_ba_behaviour (w₀ wₐ : ℝ) :
    (0 < wₐ → Tendsto (fun a => cplEOS w₀ wₐ a) atTop atBot) ∧
    (∃ M : ℝ, ∀ a : ℝ, 0 < a → |baEOS w₀ wₐ a| ≤ M) := by sorry

end DarkEnergyLCDM
Source
R. von Marttens, J. Alcaniz, S. Carneiro, "A energia escura e os desafios do modelo cosmológico padrão", Cadernos de Astronomia 7(1), 62–76 (2026), https://doi.org/10.47456/Cad.Astro.v7n1.52249, p. 72, Eqs. (19)–(20) and following text

View graph