The cosmological constant is absorbed by $\rho\to\rho-\Lambda/\kappa$ , $p\to p+\Lambda/\kappa$

Proved

FriedmannEquations.cosmological_constant_as_vacuum_energy

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

cosmologyfriedmann-equationsgeneral-relativity

Let $G>0$ and put $\kappa = 8\pi G$ (units $c=1$ ). For any $\Lambda,k$ , scale factor $R$ , density $\rho$ , pressure $p$ and time $t$ :

the first Friedmann equation with cosmological constant $\Lambda$ and density $\rho - \Lambda/\kappa$ holds at $t$ iff the first Friedmann equation with $\Lambda = 0$ and density $\rho$ holds at $t$ ;
the second Friedmann equation with cosmological constant $\Lambda$ , density $\rho - \Lambda/\kappa$ and pressure $p + \Lambda/\kappa$ holds at $t$ iff the second Friedmann equation with $\Lambda = 0$ , density $\rho$ and pressure $p$ holds at $t$ .

So the $\Lambda$ -term is the same as a fluid component with density $\Lambda/\kappa$ and pressure $-\Lambda/\kappa$ (equation of state $p = -\rho$ ).

Preamble

import Definitions.Def_FriedmannEquations_Defs
import Mathlib

open FriedmannEquations

Formal statement

theorem FriedmannEquations.cosmological_constant_as_vacuum_energy
    (G Λ k : ℝ) (hG : 0 < G) (R ρ p : ℝ → ℝ) (t : ℝ) :
    (FirstFriedmannEq G Λ k R (fun s => ρ s - Λ / (8 * Real.pi * G)) t ↔
      FirstFriedmannEq G 0 k R ρ t) ∧
    (SecondFriedmannEq G Λ R (fun s => ρ s - Λ / (8 * Real.pi * G))
        (fun s => p s + Λ / (8 * Real.pi * G)) t ↔
      SecondFriedmannEq G 0 R ρ p t) := by sorry

Source

Wikipedia, "Friedmann equations", revision oldid=1374073387, https://en.wikipedia.org/w/index.php?title=Friedmann_equations&oldid=1374073387 (the PDF supplied with this proposal), section "Cosmological constant", pp. 6–7.

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

NOTE — NON-BLIND READ-BACK. This read-back is not independent testimony. It was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source article and of the intended meaning. It was produced at the explicit request of the proposal owner. Reviewers must not treat it as a blind audit; an independent read-back is still recommended.

Fix reals $G,\Lambda,k$ with $G>0$ , functions $R,\rho,p:\mathbb R\to\mathbb R$ and a time $t$ . Let $c_\Lambda = \Lambda/(8\pi G)$ . Conclusion: both

(i) $\Big(\frac{\dot R(t)}{R(t)}\Big)^2 = \frac{8\pi G(\rho(t)-c_\Lambda)}{3} - \frac{k}{R(t)^2} + \frac{\Lambda}{3}$ iff $\Big(\frac{\dot R(t)}{R(t)}\Big)^2 = \frac{8\pi G\rho(t)}{3} - \frac{k}{R(t)^2} + \frac{0}{3}$ ;

(ii) $\frac{\ddot R(t)}{R(t)} = \frac{\Lambda}{3} - \frac{4\pi G}{3}\big((\rho(t)-c_\Lambda) + 3(p(t)+c_\Lambda)\big)$ iff $\frac{\ddot R(t)}{R(t)} = \frac{0}{3} - \frac{4\pi G}{3}\big(\rho(t)+3p(t)\big)$ .

Pointwise at the single time $t$ ; no regularity or sign assumptions on $R,\rho,p$ (derivatives are deriv, junk $0$ if not differentiable; $R(t)=0$ allowed, making the divisions $0$ ).

View graph

The cosmological constant is absorbed by ρ→ρ−Λ/κ\rho\to\rho-\Lambda/\kappaρ→ρ−Λ/κ, p→p+Λ/κp\to p+\Lambda/\kappap→p+Λ/κ

The cosmological constant is absorbed by $\rho\to\rho-\Lambda/\kappa$ , $p\to p+\Lambda/\kappa$