The centre of mass of an isolated system moves uniformly with velocity $P/M$

Proved

ConservationLaws.center_of_mass_uniform_motion

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

center-of-massconservation-lawmechanicsmomentum

Under the hypotheses of the momentum conservation milestone (masses $m_i > 0$ , internal forces obeying $F_{ij} = -F_{ji}$ , Newton's second law), and with at least one particle, let $M = \sum_i m_i$ be the total mass and $R(t) = M^{-1}\sum_i m_i x_i(t)$ the centre of mass. Then

R(t) = R(0) + t\,\frac{P(0)}{M}, \qquad P(0) = \sum_i m_i v_i(0),

i.e. the centre of mass moves in a straight line at constant velocity $v_{\mathrm{cm}} = P/M$ (equivalently $P = M v_{\mathrm{cm}}$ ).

Preamble

import Mathlib

Formal statement

namespace ConservationLaws

theorem center_of_mass_uniform_motion
    {d N : ℕ} (hN : 0 < N) (m : Fin N → ℝ) (hm : ∀ i, 0 < m i)
    (x v a : Fin N → ℝ → EuclideanSpace ℝ (Fin d))
    (F : Fin N → Fin N → ℝ → EuclideanSpace ℝ (Fin d))
    (hthird : ∀ i j t, F i j t = -F j i 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, F i j t) :
    ∀ t, (∑ i, m i)⁻¹ • ∑ i, m i • x i t =
      (∑ i, m i)⁻¹ • ∑ i, m i • x i 0 + t • ((∑ i, m i)⁻¹ • ∑ i, m i • v i 0) := by sorry

end ConservationLaws

Source

Wikipedia, "Momentum" (uploaded PDF), https://en.wikipedia.org/wiki/Momentum, section "Many particles" (centre of mass,

p = m\,v_{cm}

, Euler's first law) and section "Conservation"

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$ with $N > 0$ . Let $m_1,\dots,m_N > 0$ be reals. Let $x_i, v_i, a_i : \mathbb{R} \to \mathbb{R}^d$ (Euclidean space) and $F_{ij} : \mathbb{R} \to \mathbb{R}^d$ for all ordered pairs $(i,j)$ , including $i=j$ . Assume:

$F_{ij}(t) = -F_{ji}(t)$ for all $i,j,t$ ;
for all $i,t$ : $x_i$ is differentiable at $t$ with derivative $v_i(t)$ ;
for all $i,t$ : $v_i$ is differentiable at $t$ with derivative $a_i(t)$ ;
for all $i,t$ : $m_i a_i(t) = \sum_{j=1}^N F_{ij}(t)$ .

Write $M = \sum_i m_i$ (the statement uses $M^{-1}$ , the real reciprocal; $M > 0$ here, so this is the genuine inverse). Conclusion: for every real $t$ ,

M^{-1}\sum_i m_i x_i(t) \;=\; M^{-1}\sum_i m_i x_i(0) \;+\; t\cdot\Big(M^{-1}\sum_i m_i v_i(0)\Big).

The reference time is $0$ . Edge case $d = 0$ : everything is the zero vector.

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

The centre of mass of an isolated system moves uniformly with velocity P/MP/MP/M

The centre of mass of an isolated system moves uniformly with velocity $P/M$