Perfectly inelastic collision: common velocity and kinetic energy lost

Proved

ConservationLaws.perfectly_inelastic_collision_1d

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

collisionsenergymechanicsmomentum

Two bodies of masses $m_A, m_B > 0$ with velocities $u_A, u_B$ collide perfectly inelastically in one dimension and move afterwards with a common velocity $w$ . If momentum is conserved, $m_A u_A + m_B u_B = (m_A + m_B) w$ , then

w = \frac{m_A u_A + m_B u_B}{m_A + m_B},

and the kinetic energy lost is

\Big(\tfrac12 m_A u_A^2 + \tfrac12 m_B u_B^2\Big) - \tfrac12 (m_A + m_B) w^2 = \tfrac12\,\frac{m_A m_B}{m_A + m_B}\,(u_A - u_B)^2 \;\ge 0.

Preamble

import Mathlib

Formal statement

namespace ConservationLaws

theorem perfectly_inelastic_collision_1d
    (mA mB uA uB w : ℝ) (hmA : 0 < mA) (hmB : 0 < mB)
    (hp : mA * uA + mB * uB = (mA + mB) * w) :
    w = (mA * uA + mB * uB) / (mA + mB) ∧
    ((1 / 2 : ℝ) * mA * uA ^ 2 + (1 / 2 : ℝ) * mB * uB ^ 2) - (1 / 2 : ℝ) * (mA + mB) * w ^ 2 =
      (1 / 2 : ℝ) * (mA * mB / (mA + mB)) * (uA - uB) ^ 2 := by sorry

end ConservationLaws

Source

Wikipedia, "Momentum" (uploaded PDF), https://en.wikipedia.org/wiki/Momentum, section "Application to collisions — Inelastic collisions" (perfectly inelastic collision, conservation of momentum, kinetic energy converted to other forms)

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, w$ be real numbers with $m_A > 0$ , $m_B > 0$ , and assume

m_A u_A + m_B u_B = (m_A + m_B)\,w.

Conclusion: both

$w = \dfrac{m_A u_A + m_B u_B}{m_A + m_B}$ , and
$\Big(\tfrac12 m_A u_A^2 + \tfrac12 m_B u_B^2\Big) - \tfrac12 (m_A + m_B) w^2 = \tfrac12 \cdot \dfrac{m_A m_B}{m_A + m_B}\,(u_A - u_B)^2.$

All denominators equal $m_A + m_B > 0$ . The statement does not itself assert the inequality " $\ge 0$ "; it asserts the exact identity, whose right-hand side is a non-negative quantity.

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