Head-on elastic collision: final velocities

Proved

ConservationLaws.elastic_collision_1d

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

collisionsenergymechanicsmomentum

Two bodies of masses $m_A, m_B > 0$ collide head-on in one dimension, with velocities $u_A, u_B$ before and $v_A, v_B$ after. If both momentum and kinetic energy are conserved,

m_A u_A + m_B u_B = m_A v_A + m_B v_B,\qquad \tfrac12 m_A u_A^2 + \tfrac12 m_B u_B^2 = \tfrac12 m_A v_A^2 + \tfrac12 m_B v_B^2,

then either the velocities are unchanged ( $v_A = u_A$ , $v_B = u_B$ ), or

v_A = \frac{m_A - m_B}{m_A + m_B}u_A + \frac{2m_B}{m_A + m_B}u_B,\qquad v_B = \frac{2m_A}{m_A + m_B}u_A + \frac{m_B - m_A}{m_A + m_B}u_B.

Preamble

import Mathlib

Formal statement

namespace ConservationLaws

theorem elastic_collision_1d
    (mA mB uA uB vA vB : ℝ) (hmA : 0 < mA) (hmB : 0 < mB)
    (hp : mA * uA + mB * uB = mA * vA + mB * vB)
    (hE : (1 / 2 : ℝ) * mA * uA ^ 2 + (1 / 2 : ℝ) * mB * uB ^ 2 =
      (1 / 2 : ℝ) * mA * vA ^ 2 + (1 / 2 : ℝ) * mB * vB ^ 2) :
    (vA = uA ∧ vB = uB) ∨
    (vA = ((mA - mB) * uA + 2 * mB * uB) / (mA + mB) ∧
     vB = (2 * mA * uA + (mB - mA) * uB) / (mA + mB)) := by sorry

end ConservationLaws

Source

Wikipedia, "Momentum" (uploaded PDF), https://en.wikipedia.org/wiki/Momentum, section "Application to collisions — Elastic collisions" (head-on elastic collision, general final velocities)

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.

Let $m_A, m_B, u_A, u_B, v_A, v_B$ be real numbers with $m_A > 0$ and $m_B > 0$ . Assume

m_A u_A + m_B u_B = m_A v_A + m_B v_B

and

\tfrac12 m_A u_A^2 + \tfrac12 m_B u_B^2 = \tfrac12 m_A v_A^2 + \tfrac12 m_B v_B^2.

Conclusion: at least one of the following holds:

$v_A = u_A$ and $v_B = u_B$ ; or
$v_A = \dfrac{(m_A - m_B)u_A + 2m_B u_B}{m_A + m_B}$ and $v_B = \dfrac{2m_A u_A + (m_B - m_A)u_B}{m_A + m_B}$ .

The denominators are $m_A + m_B > 0$ , so no division by zero occurs. When $u_A = u_B$ both alternatives coincide. The statement is purely algebraic about real numbers; no time dependence or vectors appear.

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