Prove2Me

Momentum transfer for elastic scattering: ∣p⃗−p⃗′∣=2psin⁡(θ/2)|\vec p-\vec p'| = 2p\sin(\theta/2)

Proved
YukawaPotential.momentum_transfer_norm

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

mathematical-physicsyukawa-potential

Let p⃗,p⃗′∈R3\vec p,\vec p'\in\mathbb R^3 have the same length ∣p⃗∣=∣p⃗′∣=p|\vec p|=|\vec p'|=p, and let θ∈[0,π]\theta\in[0,\pi] be the angle between them. Then

∣p⃗−p⃗′∣=2p sin⁡ ⁣(12θ).|\vec p-\vec p'| = 2p\,\sin\!\bigl(\tfrac12\theta\bigr).

This is the kinematic identity used in the section Cross section after energy conservation forces ∣p⃗∣=∣p⃗′∣|\vec p|=|\vec p'|.

Formalization Note The angle is Mathlib's InnerProductGeometry.angle, i.e. arccos⁡(⟨p⃗,p⃗′⟩/(∣p⃗∣∣p⃗′∣))\arccos\bigl(\langle\vec p,\vec p'\rangle/(|\vec p||\vec p'|)\bigr); when p=0p=0 this convention gives π/2\pi/2 and both sides are 00.

Preamble
import Mathlib
import Definitions.Def_YukawaPotential_Defs

open MeasureTheory Filter Topology
Formal statement
namespace YukawaPotential
theorem momentum_transfer_norm (p : ℝ) (P P' : EuclideanSpace ℝ (Fin 3))
    (hP : ‖P‖ = p) (hP' : ‖P'‖ = p) :
    ‖P - P'‖ = 2 * p * Real.sin (InnerProductGeometry.angle P P' / 2) := by sorry
end YukawaPotential
Source
Wikipedia, "Yukawa potential", revision oldid=1371658231, https://en.wikipedia.org/w/index.php?title=Yukawa_potential&oldid=1371658231, section 'Cross section': energy conservation implies |p| = |p'| = p, so that |p - p'| = 2p sin(θ/2).
Read-back

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

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement it describes, with full knowledge of the source article and of the intended meaning. It was produced at the explicit request of the proposal owner and must not be mistaken for a blind, independent audit.

Fix a real number pp and vectors P,P′∈R3P,P'\in\mathbb R^3 with ∣P∣=p|P|=p and ∣P′∣=p|P'|=p (Euclidean norm; this forces p≥0p\ge0). Let θ\theta be the unoriented angle between PP and P′P', defined as arccos⁡(⟨P,P′⟩/(∣P∣ ∣P′∣))∈[0,π]\arccos\bigl(\langle P,P'\rangle/(|P|\,|P'|)\bigr)\in[0,\pi], where division by zero gives 00 so that θ=π/2\theta=\pi/2 if PP or P′P' is the zero vector. The statement asserts

∣P−P′∣=2p sin⁡(θ/2).|P-P'| = 2p\,\sin(\theta/2).
Human review

  • Endorsed by Shuze Chen · Oct 8, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 8, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph