Born scattering amplitude of the Yukawa potential

Proved

YukawaPotential.yukawa_born_amplitude

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

mathematical-physicsyukawa-potential

Let $\mu,\hbar,g\in\mathbb R$ , $\alpha>0$ , $m>0$ , and let $q>0$ denote the momentum transfer $|\vec p-\vec p'|$ . With $V(r)=-g^2e^{-\alpha mr}/r$ , the first Born approximation

f = \frac{-2\mu}{\hbar^2 q}\int_0^\infty r\,V(r)\,\sin(qr)\,dr

evaluates to

f = \frac{2\mu g^2}{\hbar^2\,[(\alpha m)^2+q^2]}.

This is the step "Evaluating the integral gives" in the section Cross section.

Formalization Note The integral is the Lebesgue integral over $(0,\infty)$ . No sign conditions on $\mu$ and $\hbar$ are imposed: the identity holds for all real values (for $\hbar=0$ both sides are $0$ by Lean's division convention). The case $q=0$ (forward scattering) is excluded because the article's formula divides by $|\vec p-\vec p'|$ .

Preamble

import Mathlib
import Definitions.Def_YukawaPotential_Defs

open MeasureTheory Filter Topology

Formal statement

namespace YukawaPotential
theorem yukawa_born_amplitude (μ ℏ g α m q : ℝ) (hα : 0 < α) (hm : 0 < m) (hq : 0 < q) :
    -2 * μ / (ℏ ^ 2 * q) * ∫ r in Set.Ioi (0 : ℝ), r * yukawaPotential g α m r * Real.sin (q * r) =
      2 * μ * g ^ 2 / (ℏ ^ 2 * ((α * m) ^ 2 + q ^ 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': f(θ) = -2μ/(ħ²|p-p'|) ∫_0^∞ r V(r) sin(|p-p'| r) dr; plugging in V_Yukawa and evaluating gives f(θ) = 2μg²/(ħ²[(αm)² + |p-p'|²]).

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 real numbers $\mu,\hbar,g$ (arbitrary), and real numbers $\alpha>0$ , $m>0$ , $q>0$ . Let $V(r)=-g^2e^{-\alpha m r}/r$ . The statement asserts

\frac{-2\mu}{\hbar^2 q}\cdot\int_{(0,\infty)} r\,V(r)\,\sin(qr)\,dr \;=\; \frac{2\mu g^2}{\hbar^2\bigl((\alpha m)^2+q^2\bigr)},

where the integral is the Lebesgue (Bochner) integral over the open half-line (defaulting to $0$ if the integrand were not integrable). Division by zero returns $0$ , so when $\hbar=0$ both sides are $0$ ; $\mu$ and $\hbar$ may be negative.

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