Recoil momentum and energy bounds for elastic halo-particle scattering

Proved

GoodmanWitten.recoil_bounds

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

dark-mattermathematical-physicsparticle-physics

Consider a non-relativistic elastic collision in $\mathbb R^3$ between a halo particle of mass $m>0$ with initial velocity $u$ and a nucleus of mass $M>0$ initially at rest. Let $u'$ and $V$ be the velocities of the particle and of the nucleus after the collision, so that momentum and kinetic energy are conserved:

m u = m u' + M V,\qquad \tfrac12 m|u|^2 = \tfrac12 m|u'|^2 + \tfrac12 M|V|^2 .

Then the recoil momentum and recoil kinetic energy of the nucleus satisfy

|MV| \le 2m|u|,\qquad \tfrac12 M|V|^2 \le \frac{(2m|u|)^2}{2M}.

These bounds give the largest energy a halo particle can deposit in a detector nucleus and are the basis of the paper's lower limit on detectable masses.

Preamble

import Mathlib
import Definitions.Def_GoodmanWitten_basic

Formal statement

namespace GoodmanWitten

theorem recoil_bounds (m M : ℝ) (hm : 0 < m) (hM : 0 < M)
    (u u' V : EuclideanSpace ℝ (Fin 3))
    (hmom : m • u = m • u' + M • V)
    (hen : m / 2 * ‖u‖ ^ 2 = m / 2 * ‖u'‖ ^ 2 + M / 2 * ‖V‖ ^ 2) :
    ‖M • V‖ ≤ maxRecoilMomentum m ‖u‖ ∧
      M / 2 * ‖V‖ ^ 2 ≤ maxRecoilEnergy m M ‖u‖ := by sorry

end GoodmanWitten

Source

M. W. Goodman and E. Witten, Detectability of certain dark-matter candidates, Phys. Rev. D 31, 3059-3063 (1985), https://doi.org/10.1103/PhysRevD.31.3059, p. 3059, right column, paragraph 2

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph