Prove2Me

Electrostatic model identity for the momentum law (p. 14)

Proved
EinsteinGrossmann1913.electrostatic_momentum_identity

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

entwurf-theorygeneral-relativityhistory-of-physicstensor-calculus

Let φ:R3→R\varphi:\mathbb R^3\to\mathbb R be a twice continuously differentiable function (the electrostatic potential). Then for every ν∈{1,2,3}\nu\in\{1,2,3\} and every point xx,

∑μ∂∂xμ(∂φ∂xν∂φ∂xμ)−∂∂xν(12∑μ(∂φ∂xμ)2)=∂φ∂xν∑μ∂2φ∂xμ2.\sum_{\mu}\frac{\partial}{\partial x_\mu}\Big(\frac{\partial\varphi}{\partial x_\nu}\frac{\partial\varphi}{\partial x_\mu}\Big)-\frac{\partial}{\partial x_\nu}\Big(\tfrac12\sum_\mu\Big(\frac{\partial\varphi}{\partial x_\mu}\Big)^2\Big)=\frac{\partial\varphi}{\partial x_\nu}\sum_\mu\frac{\partial^2\varphi}{\partial x_\mu^2}.

In the source this identity is the model for the method by which the gravitational field equations are found: if φ\varphi satisfies ∑μ∂2φ/∂xμ2=ϱ\sum_\mu\partial^2\varphi/\partial x_\mu^2=\varrho, the right-hand side equals ∂φ∂xνϱ\frac{\partial\varphi}{\partial x_\nu}\varrho, the negative of the momentum −∂φ∂xνϱ-\frac{\partial\varphi}{\partial x_\nu}\varrho transferred to the charges, so the momentum law takes the form of a sum of derivatives.

Formalization Note Only the identity itself is stated; the Poisson equation is not assumed.

Preamble
import Mathlib
import Definitions.Def_EinsteinGrossmann1913_Defs
Formal statement
namespace EinsteinGrossmann1913

theorem electrostatic_momentum_identity (φ : (Fin 3 → ℝ) → ℝ) (hφ : ContDiff ℝ 2 φ)
    (ν : Fin 3) (x : Fin 3 → ℝ) :
    (∑ μ : Fin 3, pd μ (fun y => pd ν φ y * pd μ φ y) x)
      - pd ν (fun y => (1 / 2) * ∑ μ : Fin 3, (pd μ φ y) ^ 2) x
      = pd ν φ x * ∑ μ : Fin 3, pd μ (pd μ φ) x := 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. 14 (electrostatic example illustrating the method).
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.

For every function φ:R3→R\varphi:\mathbb R^3\to\mathbb R that is C2C^2 on all of R3\mathbb R^3, every index ν∈{1,2,3}\nu\in\{1,2,3\} and every point x∈R3x\in\mathbb R^3, the statement asserts the equality of real numbers

∑μ=13∂μ(y↦∂νφ(y) ∂μφ(y))(x)−∂ν(y↦12∑μ=13(∂μφ(y))2)(x)=∂νφ(x)∑μ=13∂μ(∂μφ)(x),\sum_{\mu=1}^{3}\partial_\mu\big(y\mapsto\partial_\nu\varphi(y)\,\partial_\mu\varphi(y)\big)(x)-\partial_\nu\Big(y\mapsto\tfrac12\sum_{\mu=1}^3(\partial_\mu\varphi(y))^2\Big)(x)=\partial_\nu\varphi(x)\sum_{\mu=1}^3\partial_\mu(\partial_\mu\varphi)(x),

where ∂ih(x)\partial_i h(x) is the Fréchet derivative of hh at xx applied to the ii-th standard basis vector (defined to be 00 where hh is not differentiable). No other hypothesis appears; in particular nothing about a charge density is assumed.

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