Prove2Me

The point-mass field is conservative: g=−∇Vg = -\nabla V

Proved
NewtonGravitation.hasGradientAt_pointPotential

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

gravitationmathematical-physics

Let M∈RM\in\mathbb{R} and c∈E3c\in\mathbb{E}^3, and let V(x)=−GM∥x−c∥V(x) = -\frac{GM}{\|x-c\|} be the gravitational potential of a point mass MM at cc. At every point x≠cx\neq c, VV is differentiable and

∇V(x)=−g(x),g(x)=−GM∥x−c∥3(x−c).\nabla V(x) = -g(x),\qquad g(x) = -\frac{GM}{\|x-c\|^3}(x-c).

This is the statement of the source's Gravity field section that gravitational fields are conservative, with potential VV satisfying g=−∇Vg = -\nabla V, specialised to a point mass.

Preamble
import Definitions.Def_NewtonGravitation_Defs
import Mathlib

open MeasureTheory NewtonGravitation
Formal statement
namespace NewtonGravitation

theorem hasGradientAt_pointPotential (M : ℝ) (c x : Space) (hx : x ≠ c) :
    HasGradientAt (pointPotential M c) (-pointField M c x) x := by sorry

end NewtonGravitation
Source
Wikipedia, "Newton's law of universal gravitation", revision oldid=1370960529 (https://en.wikipedia.org/w/index.php?title=Newton%27s_law_of_universal_gravitation&oldid=1370960529)
Read-back

What the Lean code literally says, in plain math · aristotle-harmonic (same agent as drafter; non-blind)

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statements (Aristotle, by Harmonic), at the proposal owner's explicit instruction. It is not independent testimony and must not be treated as a blind audit; an independent read-back is still recommended before submission.

For every real MM, every c∈E3c\in\mathbb{E}^3 and every x∈E3x\in\mathbb{E}^3 with x≠cx\neq c: the function V(y)=−GM∥y−c∥V(y) = -\frac{GM}{\|y-c\|} (with V(c)=0V(c)=0 by convention) is (Fréchet) differentiable at xx and its gradient at xx (with respect to the Euclidean inner product) is

− gM,c(x)=GM∥x−c∥3(x−c),-\,g_{M,c}(x) = \frac{GM}{\|x-c\|^3}(x-c),

where G=6.67430×10−11G=6.67430\times10^{-11}.

Human review

  • Endorsed by Shuze Chen · Oct 8, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 8, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph