Prove2Me

Radiation density scales as a−4a^{-4}

Proved
DarkEnergyLCDM.radiation_density_scaling

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

cosmologymathematical-physics

Let II be an open connected interval, and let aa and ρ\rho be differentiable on II with a>0a>0 there. Suppose ρ\rho satisfies the continuity equation with the radiation equation of state p=ρ/3p=\rho/3:

ρ˙+3H(ρ+ρ3)=0on I.\dot\rho + 3H\left(\rho + \tfrac{\rho}{3}\right) = 0 \quad\text{on } I.

If t0∈It_0\in I and a(t0)=1a(t_0)=1, then ρ(t)=ρ(t0) a(t)−4\rho(t) = \rho(t_0)\,a(t)^{-4} for all t∈It\in I.

This is the first half of Eq. (4): radiation dilutes as a−4a^{-4}.

Preamble
import Mathlib
import Definitions.Def_DarkEnergyLCDM_Defs
Formal statement
namespace DarkEnergyLCDM

theorem radiation_density_scaling (I : Set ℝ) (hI : IsOpen I) (hIc : IsPreconnected I)
    (a ρ : ℝ → ℝ) (ha : DifferentiableOn ℝ a I) (ha_pos : ∀ t ∈ I, 0 < a t)
    (hρ : DifferentiableOn ℝ ρ I)
    (hcont : ∀ t ∈ I, ContinuityEq a ρ (fun s => ρ s / 3) t)
    (t₀ : ℝ) (ht₀ : t₀ ∈ I) (ha₀ : a t₀ = 1) :
    ∀ t ∈ I, ρ t = ρ t₀ * (a t)⁻¹ ^ 4 := 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. (4) (radiation, wr=1/3w_r = 1/3)

View graph