Eq. (19): matter and gravitational field together satisfy the conservation laws

Proved

EinsteinGrossmann1913.total_conservation

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

entwurf-theorygeneral-relativityhistory-of-physicstensor-calculus

Let $g_{\mu\nu}$ be a fundamental tensor on $\mathbb R^4$ (twice continuously differentiable, symmetric, $g=\det(g_{\mu\nu})<0$ ), let $\kappa\neq0$ , and let $\Theta_{\mu\nu}$ be a continuously differentiable contravariant stress-energy tensor of a material process such that

the energy-momentum law of matter (10) holds:

\sum_{\mu\nu}\frac{\partial}{\partial x_\nu}\big(\sqrt{-g}\,g_{\sigma\mu}\Theta_{\mu\nu}\big)-\tfrac12\sum_{\mu\nu}\sqrt{-g}\,\frac{\partial g_{\mu\nu}}{\partial x_\sigma}\Theta_{\mu\nu}=0;

the Entwurf gravitational field equations (18) hold: $\Delta_{\mu\nu}(\gamma)=\kappa(\Theta_{\mu\nu}+\vartheta_{\mu\nu})$ , with $\vartheta_{\mu\nu}$ the stress-energy tensor of the gravitational field, eq. (13), and $\Delta_{\mu\nu}$ the operator of eq. (15).

Then for every $\sigma=1,2,3,4$ and every point

\sum_{\mu\nu}\frac{\partial}{\partial x_\nu}\Big\{\sqrt{-g}\,g_{\sigma\mu}\,(\Theta_{\mu\nu}+\vartheta_{\mu\nu})\Big\}=0.

In the words of the source: “Hieraus ersieht man, daß für Materie und Gravitationsfeld zusammen die Erhaltungssätze gelten.” The gravitational stress-energy $\vartheta_{\mu\nu}$ enters the field equations in the same way as $\Theta_{\mu\nu}$ , and the total energy-momentum of matter and field is conserved.

Formalization Note Everything is stated in one global chart on $\mathbb R^4$ ; $\Theta$ is assumed $C^1$ so that the derivatives in (10) and in the conclusion are genuine derivatives.

Preamble

import Mathlib
import Definitions.Def_EinsteinGrossmann1913_Defs

Formal statement

namespace EinsteinGrossmann1913

theorem total_conservation (κ : ℝ) (hκ : κ ≠ 0) (g Θ : Field2) (hg : IsMetricField g)
    (hΘ : ∀ μ ν : Fin 4, ContDiff ℝ 1 (fun x => Θ x μ ν))
    (h10 : MatterConservation g Θ) (h18 : EntwurfFieldEquations κ g Θ)
    (σ : Fin 4) (x : Coord) :
    ∑ μ : Fin 4, ∑ ν : Fin 4,
      pd ν (fun y => sqrtNegDet g y * g y σ μ
        * (Θ y μ ν + gravStressEnergy κ g y μ ν)) x = 0 := by sorry

end EinsteinGrossmann1913

Source

A. Einstein and M. Grossmann, "Entwurf einer verallgemeinerten Relativitätstheorie und einer Theorie der Gravitation", B. G. Teubner, Leipzig und Berlin 1913 (Separatabdruck aus Zeitschrift für Mathematik und Physik 62), Part I (Physikalischer Teil, A. Einstein), §5, p. 17, eq. (19), derived from eqs. (10), (12a) and (18).

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 paper 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.

Let $\kappa$ be a real number with $\kappa\neq0$ . $g$ is an arbitrary map assigning to every point $x\in\mathbb R^4$ a real $4\times4$ matrix $(g_{\mu\nu}(x))$ , and the hypothesis IsMetricField $g$ requires exactly: every entry $x\mapsto g_{\mu\nu}(x)$ is $C^2$ on all of $\mathbb R^4$ ; $g_{\mu\nu}(x)=g_{\nu\mu}(x)$ for all $x,\mu,\nu$ ; and $\det(g_{\mu\nu}(x))<0$ for every $x$ . No signature condition beyond the sign of the determinant is imposed. $\Theta$ is a map $x\mapsto(\Theta_{\mu\nu}(x))$ into real $4\times4$ matrices with every entry $C^1$ on $\mathbb R^4$ (no symmetry assumed). Throughout, $\partial_i f(x)$ is the Fréchet derivative of $f$ at $x$ applied to the $i$ -th standard basis vector (by convention it is $0$ wherever $f$ is not differentiable), $\gamma_{\mu\nu}(x)$ denotes the entries of the matrix inverse of $(g_{\mu\nu}(x))$ , $\sqrt{-g}$ is the real square root of $-\det(g_{\mu\nu}(x))$ , and $1/0$ is read as $0$ . Indices range over four values (in the code $0,1,2,3$ ; index $3$ plays the role of the source's $x_4$ ).

Hypotheses:

(eq. (10)) for every $\sigma$ and every $x$ : $\sum_{\mu,\nu}\partial_\nu\big(y\mapsto\sqrt{-g}(y)\,g_{\sigma\mu}(y)\Theta_{\mu\nu}(y)\big)(x)-\frac12\sum_{\mu,\nu}\sqrt{-g}(x)\,\partial_\sigma g_{\mu\nu}(x)\,\Theta_{\mu\nu}(x)=0$ ;
(eq. (18)) for every $x,\mu,\nu$ : $\Delta_{\mu\nu}(x)=\kappa\big(\Theta_{\mu\nu}(x)+\vartheta_{\mu\nu}(x)\big)$ , where $\vartheta_{\mu\nu}=-\frac{1}{2\kappa}\sum_{\alpha,\beta,\tau,\rho}\big(\gamma_{\alpha\mu}\gamma_{\beta\nu}-\tfrac12\gamma_{\mu\nu}\gamma_{\alpha\beta}\big)\partial_\alpha g_{\tau\rho}\,\partial_\beta\gamma_{\tau\rho}$ and $\Delta_{\mu\nu}=\sum_{\alpha,\beta}\frac{1}{\sqrt{-g}}\partial_\alpha\big(\gamma_{\alpha\beta}\sqrt{-g}\,\partial_\beta\gamma_{\mu\nu}\big)-\sum_{\alpha,\beta,\tau,\rho}\gamma_{\alpha\beta}g_{\tau\rho}\,\partial_\alpha\gamma_{\mu\tau}\,\partial_\beta\gamma_{\nu\rho}$ .

Conclusion: for the given index $\sigma$ and point $x$ ,

\sum_{\mu,\nu}\partial_\nu\Big(y\mapsto\sqrt{-g}(y)\,g_{\sigma\mu}(y)\big(\Theta_{\mu\nu}(y)+\vartheta_{\mu\nu}(y)\big)\Big)(x)=0.

The hypotheses can be met, e.g. by a constant matrix field $g$ with negative determinant together with $\Theta\equiv0$ .

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