Vacuum energy density and pressure

Proved

EinsteinFieldEquationsD.vacuumStressEnergy_eq_perfectFluid

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

differential-geometryeinstein-field-equationsgeneral-relativity

The vacuum stress–energy tensor $T^{(\mathrm{vac})}_{\mu\nu}=-\frac\Lambda\kappa g_{\mu\nu}$ is the stress–energy tensor of a perfect fluid with constant energy density and isotropic pressure

\rho_{\mathrm{vac}}=-p_{\mathrm{vac}}=\frac\Lambda\kappa,

for any velocity field $u$ : $T^{(\mathrm{vac})}_{\mu\nu}=(\rho_{\mathrm{vac}}+p_{\mathrm{vac}})u_\mu u_\nu+p_{\mathrm{vac}}g_{\mu\nu}$ .

Preamble

import Mathlib
import Definitions.Def_EinsteinFieldEquationsD_Defs

Formal statement

namespace EinsteinFieldEquationsD

theorem vacuumStressEnergy_eq_perfectFluid {D : ℕ} (g : Tensor2 D) (Λ κ : ℝ) (u : Coord D → Fin D → ℝ) :
    vacuumStressEnergy g Λ κ = perfectFluid g (Λ / κ) (-(Λ / κ)) u := 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$ is an arbitrary matrix-valued function on $\mathbb{R}^D$ (no assumptions), $\Lambda,\kappa$ are arbitrary reals (including $\kappa=0$ , where $\Lambda/\kappa$ is $0$ ), and $u$ is an arbitrary field assigning to each point a vector $(u_a(x))\in\mathbb{R}^D$ (no normalization such as $g^{ab}u_au_b=-1$ is imposed).

Claim. As functions of $(x,a,b)$ ,

-\frac\Lambda\kappa\,g_{ab}(x)=\Big(\frac\Lambda\kappa+\Big(-\frac\Lambda\kappa\Big)\Big)u_a(x)u_b(x)+\Big(-\frac\Lambda\kappa\Big)g_{ab}(x).

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