Isolated $N$ -body system with pair potentials: momentum and energy are conserved

Proved

ConservationLaws.nbody_momentum_and_energy_conservation

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

conservation-lawenergymechanicsmomentumn-body

Let $N$ particles in $\mathbb{R}^d$ with masses $m_i > 0$ interact only through pair potentials $\varphi_{ij} = \varphi_{ji}$ , each differentiable on $(0,\infty)$ , so that along a collision-free trajectory ( $x_i(t) \ne x_j(t)$ for $i \ne j$ ) Newton's second law reads

m_i\,\ddot x_i(t) = \sum_{j \ne i} -\varphi_{ij}'\big(\|x_i(t)-x_j(t)\|\big)\,\frac{x_i(t)-x_j(t)}{\|x_i(t)-x_j(t)\|}.

Then the total momentum $\sum_i m_i \dot x_i(t)$ and the total mechanical energy

E(t) = \sum_i \tfrac12 m_i\|\dot x_i(t)\|^2 + \sum_{i<j}\varphi_{ij}\big(\|x_i(t)-x_j(t)\|\big)

are both constant in time.

Preamble

import Mathlib

Formal statement

namespace ConservationLaws

theorem nbody_momentum_and_energy_conservation
    {d N : ℕ} (m : Fin N → ℝ) (hm : ∀ i, 0 < m i)
    (φ : Fin N → Fin N → ℝ → ℝ) (hφsym : ∀ i j, φ i j = φ j i)
    (hφdiff : ∀ i j, ∀ r : ℝ, 0 < r → DifferentiableAt ℝ (φ i j) r)
    (x v a : Fin N → ℝ → EuclideanSpace ℝ (Fin d))
    (hnc : ∀ t i j, i ≠ j → x i t ≠ x j t)
    (hx : ∀ i t, HasDerivAt (x i) (v i t) t)
    (hv : ∀ i t, HasDerivAt (v i) (a i t) t)
    (hnewton : ∀ i t, m i • a i t = ∑ j ∈ Finset.univ.erase i,
      (-(deriv (φ i j) ‖x i t - x j t‖) / ‖x i t - x j t‖) • (x i t - x j t)) :
    (∀ t s, ∑ i, m i • v i t = ∑ i, m i • v i s) ∧
    (∀ t s,
      (∑ i, (1 / 2 : ℝ) * m i * ‖v i t‖ ^ 2 + ∑ i, ∑ j ∈ Finset.Ioi i, φ i j ‖x i t - x j t‖) =
      (∑ i, (1 / 2 : ℝ) * m i * ‖v i s‖ ^ 2 + ∑ i, ∑ j ∈ Finset.Ioi i, φ i j ‖x i s - x j s‖)) := by sorry

end ConservationLaws

Source

Wikipedia, "Momentum" (uploaded PDF), https://en.wikipedia.org/wiki/Momentum, section "Conservation"; Wikipedia, "Conservation of energy" (uploaded PDF), https://en.wikipedia.org/wiki/Conservation_of_energy (conservation of kinetic plus potential energy in a closed system)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as drafter, non-blind

Disclosure: NON-BLIND read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source material and of the intended meaning. It is not independent or blind testimony and must not be treated as such by any reviewer. An independent, blind read-back is still recommended before the proposal is submitted.

Fix natural numbers $d$ and $N$ and index particles by $i \in \{1,\dots,N\}$ (with the usual order). Let $m_i > 0$ be reals. Let $\varphi_{ij} : \mathbb{R} \to \mathbb{R}$ for every ordered pair $(i,j)$ (including $i = j$ ), with $\varphi_{ij} = \varphi_{ji}$ as functions, and with $\varphi_{ij}$ differentiable at every $r > 0$ (nothing is assumed at $r \le 0$ ). Let $x_i, v_i, a_i : \mathbb{R} \to \mathbb{R}^d$ (Euclidean space). Assume:

No collisions: $x_i(t) \ne x_j(t)$ whenever $i \ne j$ , for all $t$ ;
for all $i,t$ : $x_i$ is differentiable at $t$ with derivative $v_i(t)$ , and $v_i$ is differentiable at $t$ with derivative $a_i(t)$ ;
for all $i,t$ , writing $r_{ij}(t) = \|x_i(t) - x_j(t)\|$ :

m_i\, a_i(t) = \sum_{j \ne i} \left(\frac{-\varphi_{ij}'(r_{ij}(t))}{r_{ij}(t)}\right)(x_i(t) - x_j(t)),

where $\varphi_{ij}'(r)$ denotes the derivative of $\varphi_{ij}$ at $r$ (by 1, $r_{ij}(t) > 0$ for $j \ne i$ , so this derivative exists and the division is genuine).

Conclusion — both of the following:

for all real $t, s$ : $\displaystyle\sum_i m_i v_i(t) = \sum_i m_i v_i(s)$ ;
for all real $t, s$ :

\sum_i \tfrac12 m_i\|v_i(t)\|^2 + \sum_{i}\sum_{j > i}\varphi_{ij}(r_{ij}(t)) = \sum_i \tfrac12 m_i\|v_i(s)\|^2 + \sum_{i}\sum_{j > i}\varphi_{ij}(r_{ij}(s)).

The potential energy sums each unordered pair once ( $j > i$ ). The diagonal functions $\varphi_{ii}$ never enter. Edge cases: $N = 0$ or $N = 1$ make all force sums empty; $d = 0$ with $N \ge 2$ makes the no-collision hypothesis unsatisfiable (all points coincide), so the statement is vacuous in that case only.

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

Isolated NNN-body system with pair potentials: momentum and energy are conserved

Isolated $N$ -body system with pair potentials: momentum and energy are conserved