Cosmological term as vacuum stress–energy

Proved

EinsteinFieldEquationsD.cosmological_constant_as_vacuum_energy

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

differential-geometryeinstein-field-equationsgeneral-relativity

Let $\kappa\neq0$ . For any fields $g,T$ , any $\Lambda$ and any set $U$ , the field equations $G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu}$ hold on $U$ if and only if

G_{\mu\nu}=\kappa\big(T_{\mu\nu}+T^{(\mathrm{vac})}_{\mu\nu}\big)\quad\text{on }U,\qquad T^{(\mathrm{vac})}_{\mu\nu}=-\frac\Lambda\kappa g_{\mu\nu}.

Preamble

import Mathlib
import Definitions.Def_EinsteinFieldEquationsD_Defs

Formal statement

namespace EinsteinFieldEquationsD

theorem cosmological_constant_as_vacuum_energy {D : ℕ} (g T : Tensor2 D) (U : Set (Coord D)) (Λ κ : ℝ) (hκ : κ ≠ 0) :
    EinsteinFieldEquationsOn g T Λ κ U ↔
      ∀ x ∈ U, ∀ a b : Fin D,
        einsteinTensor g x a b = κ * (T x a b + vacuumStressEnergy g Λ κ x a b) := by sorry

end EinsteinFieldEquationsD

Source

Wikipedia, "Einstein field equations", revision oldid=1374672993, https://en.wikipedia.org/w/index.php?title=Einstein_field_equations&oldid=1374672993; section 'Cosmological constant'

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 (Aristotle, by Harmonic) that drafted the Lean statements it describes, with full knowledge of the source and of the intended meaning. It is not the output of a blind, independent auditor, and no reviewer should treat it as such. Compare it against the Lean code yourself.

Here $D$ is arbitrary, $g$ and $T$ are arbitrary matrix-valued functions on $\mathbb{R}^D$ (no smoothness, symmetry or nondegeneracy is assumed), $U$ is an arbitrary subset of $\mathbb{R}^D$ , $\Lambda$ is any real, and $\kappa$ is a real with $\kappa\neq0$ .

Claim. The statement "for all $x\in U$ and all $a,b$ : $G_{ab}(x)+\Lambda g_{ab}(x)=\kappa T_{ab}(x)$ " is equivalent to the statement "for all $x\in U$ and all $a,b$ : $G_{ab}(x)=\kappa\big(T_{ab}(x)-(\Lambda/\kappa)g_{ab}(x)\big)$ ". $G$ is the Einstein tensor computed from $g$ by the coordinate formulas (which are defined for any $g$ ).

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph