Force from the field: $F = m\,g(r)$

Proved

NewtonGravitation.pointForce_eq_smul_pointField

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

gravitationmathematical-physics

Let $m_1,m_2\in\mathbb{R}$ and $r_1,r_2\in\mathbb{E}^3$ , and let $g$ be the gravitational field of the point mass $m_1$ at $r_1$ , $g(x) = -\frac{G m_1}{\|x-r_1\|^3}(x-r_1)$ . Then the force exerted on the body of mass $m_2$ at $r_2$ is

F_{21} = m_2\, g(r_2).

This is the identity $F = m\,g(r)$ of the source's Gravity field section: the field is the force per unit mass.

Preamble

import Definitions.Def_NewtonGravitation_Defs
import Mathlib

open MeasureTheory NewtonGravitation

Formal statement

namespace NewtonGravitation

theorem pointForce_eq_smul_pointField (m₁ m₂ : ℝ) (r₁ r₂ : Space) :
    pointForce m₁ m₂ r₁ r₂ = m₂ • pointField m₁ r₁ r₂ := 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 all real numbers $m_1, m_2$ and all points $r_1, r_2\in\mathbb{E}^3$ (possibly equal),

F(m_1,m_2,r_1,r_2) = m_2\cdot g_{m_1,r_1}(r_2),

where $F(m_1,m_2,r_1,r_2) = -\frac{G m_1 m_2}{\|r_2-r_1\|^2}\|r_2-r_1\|^{-1}(r_2-r_1)$ , $g_{M,c}(x) = -\frac{GM}{\|x-c\|^3}(x-c)$ , $G=6.67430\times10^{-11}$ , and division by zero gives $0$ (both sides vanish when $r_1=r_2$ ).

View graph

Force from the field: F=m g(r)F = m\,g(r)F=mg(r)

Force from the field: $F = m\,g(r)$