Prove2Me

Acceleration equation in effective variables

Proved
CosmologyEOS.effective_acceleration_equation

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

cosmologymathematical-physics

Let G≠0G\neq 0 and Λ\Lambda be real, and let a,ε,pa,\varepsilon,p be real functions of time. Define the effective energy density and pressure ε′=ε+Λ8πG\varepsilon' = \varepsilon + \frac{\Lambda}{8\pi G} and p′=p−Λ8πGp' = p - \frac{\Lambda}{8\pi G}. Then at every time tt:

  1. the acceleration equation 3a¨a=Λ−4πG(ε+3p)3\frac{\ddot a}{a} = \Lambda - 4\pi G(\varepsilon + 3p) holds if and only if
a¨a=−43πG (ε′+3p′);\frac{\ddot a}{a} = -\frac43\pi G\,(\varepsilon' + 3p');
  1. if ε′≠0\varepsilon'\neq 0 and w′=p′/ε′w' = p'/\varepsilon', then
−43πG (ε′+3p′)=−43πG (1+3w′) ε′.-\frac43\pi G\,(\varepsilon'+3p') = -\frac43\pi G\,(1+3w')\,\varepsilon'.

This expresses the effect of the cosmological constant as a shift of the fluid variables.

Formalization Note No sign or regularity hypotheses are needed: the statement is an identity between the two forms of the equation at a single time.

Preamble
import Mathlib
import Definitions.Def_CosmologyEOS_Defs

open Real Filter Topology
Formal statement
namespace CosmologyEOS

theorem effective_acceleration_equation (G Λ : ℝ) (hG : G ≠ 0) (a ε p : ℝ → ℝ) (t : ℝ) :
    (AccelerationEquation G Λ a ε p t ↔
      deriv (deriv a) t / a t =
        -(4 / 3) * π * G *
          (effectiveEnergyDensity G Λ (ε t) + 3 * effectivePressure G Λ (p t))) ∧
    (effectiveEnergyDensity G Λ (ε t) ≠ 0 →
      -(4 / 3) * π * G *
          (effectiveEnergyDensity G Λ (ε t) + 3 * effectivePressure G Λ (p t)) =
        -(4 / 3) * π * G *
          (1 + 3 * eosParameter (effectivePressure G Λ (p t)) (effectiveEnergyDensity G Λ (ε t))) *
          effectiveEnergyDensity G Λ (ε t)) := by
  sorry

end CosmologyEOS
Source
Wikipedia, "Equation of state (cosmology)", revision 1375011367, https://en.wikipedia.org/w/index.php?title=Equation_of_state_(cosmology)&oldid=1375011367, section 'FLRW equations and the equation of state' (Friedmann acceleration equation, effective ε', p', w')
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; NON-BLIND

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent that drafted the Lean statement below, with full knowledge of the source text and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; reviewers should compare the Lean code with the source themselves.

Let G,Λ∈RG,\Lambda\in\mathbb R with G≠0G\ne 0, let a,ε,p:R→Ra,\varepsilon,p:\mathbb R\to\mathbb R and t∈Rt\in\mathbb R. Write q=a′′(t)/a(t)q = a^{\prime\prime}(t)/a(t) (second derivative with the convention that non-differentiability gives 00; x/0=0x/0 = 0), E=ε(t)+Λ8πGE = \varepsilon(t) + \dfrac{\Lambda}{8\pi G} and P=p(t)−Λ8πGP = p(t) - \dfrac{\Lambda}{8\pi G}. The statement asserts both:

  1. 3q=Λ−4πG(ε(t)+3p(t))3q = \Lambda - 4\pi G(\varepsilon(t)+3p(t)) holds if and only if q=−43πG (E+3P)q = -\tfrac43\pi G\,(E + 3P);
  2. if E≠0E\ne 0, then −43πG (E+3P)=−43πG (1+3 PE)E-\tfrac43\pi G\,(E + 3P) = -\tfrac43\pi G\,\bigl(1 + 3\,\tfrac{P}{E}\bigr)E.

No differentiability, positivity of aa, or sign condition on GG is assumed (only G≠0G\neq0).

Human review

View graph