Cut-off vacuum energy $\sim k_{\lim}^4/(16\pi^2)$

Proved

DarkEnergyLCDM.vacuum_energy_cutoff_asymptotics

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

cosmologymathematical-physics

For a field of mass $m$ , let

\rho_{\rm vac}(k_{\lim}) = \int_{\{k\in\mathbb R^3:\ |k|\le k_{\lim}\}} \frac12\sqrt{|k|^2+m^2}\;\frac{d^3k}{(2\pi)^3}.

Then

\lim_{k_{\lim}\to\infty} \frac{\rho_{\rm vac}(k_{\lim})}{k_{\lim}^4/(16\pi^2)} = 1,

that is, $\rho_{\rm vac}\approx k_{\lim}^4/(16\pi^2)$ for $k_{\lim}\gg m$ .

This is the quantum-field-theory estimate of the vacuum energy behind the cosmological-constant problem, Eq. (10).

Formalization Note The printed Eq. (10) omits the zero-point factor $\frac12$ . Without it the integral is asymptotic to $k_{\lim}^4/(8\pi^2)$ , not to the stated $k_{\lim}^4/(16\pi^2)$ . The factor $\frac12$ is included here.

Preamble

import Mathlib
import Definitions.Def_DarkEnergyLCDM_Defs

Formal statement

namespace DarkEnergyLCDM

open Real Filter Topology

theorem vacuum_energy_cutoff_asymptotics (m : ℝ) :
    Tendsto (fun klim : ℝ => vacuumEnergyCutoff m klim / (klim ^ 4 / (16 * π ^ 2)))
      atTop (𝓝 1) := 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. 65, Eq. (10)

View graph

Cut-off vacuum energy ∼klim⁡4/(16π2)\sim k_{\lim}^4/(16\pi^2)∼klim4​/(16π2)

Cut-off vacuum energy $\sim k_{\lim}^4/(16\pi^2)$