Eq. (2): thermally regularized vacuum density
ProvedCarneiroDeSitter.bose_integral_vacuum_densitycosmologymathematical-physics
Let be a cutoff (characteristic temperature). Then the Bose–Einstein regularized vacuum energy integral is
This is the exact form of Carneiro's estimate (Eq. (2)): a thermal distribution of vacuum modes at temperature regularizes the divergent flat-space vacuum density and gives a density proportional to .
Formalization Note The integral is the Lebesgue integral over ; the paper writes , and the theorem states the exact constant .
Preamble
import Mathlib import Definitions.Def_CarneiroDeSitter2006 open Real Filter Topology Asymptotics MeasureTheory Set
Formal statement
namespace CarneiroDeSitter
theorem bose_integral_vacuum_density (m : ℝ) (hm : 0 < m) :
∫ ω in Ioi (0 : ℝ), ω ^ 3 / (Real.exp (ω / m) - 1) = π ^ 4 / 15 * m ^ 4 := by sorry
end CarneiroDeSitterSource
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. 2242, Eq. (2)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.