Trace-reversed form of the Einstein field equations

Proved

EinsteinFieldEquationsD.field_equations_iff_trace_reversed

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

differential-geometryeinstein-field-equationsgeneral-relativity

Let $D\neq2$ , let $g$ be a smooth, symmetric, nondegenerate metric on an open set $U\subseteq\mathbb{R}^D$ and $x\in U$ . Then at $x$ the Einstein field equations are equivalent to their trace-reversed form:

G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu}\ \ \forall\mu,\nu\iff R_{\mu\nu}-\frac2{D-2}\Lambda g_{\mu\nu}=\kappa\Big(T_{\mu\nu}-\frac1{D-2}Tg_{\mu\nu}\Big)\ \ \forall\mu,\nu,

with $T=g^{\mu\nu}T_{\mu\nu}$ . (For $D=4$ : $R_{\mu\nu}-\Lambda g_{\mu\nu}=\kappa(T_{\mu\nu}-\tfrac12Tg_{\mu\nu})$ .)

Preamble

import Mathlib
import Definitions.Def_EinsteinFieldEquationsD_Defs

Formal statement

namespace EinsteinFieldEquationsD

theorem field_equations_iff_trace_reversed {D : ℕ} (hD : D ≠ 2) (g T : Tensor2 D) (U : Set (Coord D)) (Λ κ : ℝ)
    (hg : IsMetricOn g U) (x : Coord D) (hx : x ∈ U) :
    (∀ a b : Fin D, einsteinTensor g x a b + Λ * g x a b = κ * T x a b) ↔
      (∀ a b : Fin D, ricci g x a b - (2 / ((D : ℝ) - 2)) * Λ * g x a b
        = κ * (T x a b - (1 / ((D : ℝ) - 2)) * metricTrace g T x * 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 'Equivalent formulations', second and third displays

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 an arbitrary natural number, points are $x \in \mathbb{R}^D$ , $g$ is any function assigning to each point a real $D\times D$ matrix $(g_{ab}(x))$ , and $U \subseteq \mathbb{R}^D$ is any set. The hypothesis that $g$ is a metric on $U$ means: $U$ is open; every component $x \mapsto g_{ab}(x)$ is $C^\infty$ on $U$ ; $g_{ab}(x) = g_{ba}(x)$ for $x \in U$ ; and $\det g(x) \neq 0$ for $x \in U$ . No signature (Lorentzian or otherwise) is imposed. Outside $U$ , $g$ is unconstrained.

Additionally: $D\neq2$ ; $T$ is an arbitrary 2-tensor field; $\Lambda,\kappa$ arbitrary reals; $x$ is a point of $U$ .

Claim. The following are equivalent:

for all $a,b$ : $G_{ab}(x)+\Lambda g_{ab}(x)=\kappa T_{ab}(x)$ ;
for all $a,b$ : $R_{ab}(x)-\dfrac{2}{D-2}\Lambda g_{ab}(x)=\kappa\Big(T_{ab}(x)-\dfrac1{D-2}\Big(\sum_{c,d}g^{cd}(x)T_{cd}(x)\Big)g_{ab}(x)\Big)$ .

Both conditions concern the single point $x$ only. For $D=0$ both sides are vacuously true; for $D=1$ the coefficients are $2/(-1)$ and $1/(-1)$ .

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