Total Born cross section of the Yukawa potential

Proved

YukawaPotential.yukawa_total_cross_section

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

mathematical-physicsyukawa-potential

Let $\mu,\hbar,g,p\in\mathbb R$ , $\alpha>0$ and $m>0$ . Then

\int_0^\pi \frac{4\mu^2g^4}{\hbar^4}\cdot\frac{2\pi\sin\theta}{\bigl[(\alpha m)^2+4p^2\sin^2(\tfrac12\theta)\bigr]^2}\,d\theta \;=\; \frac{4\mu^2g^4}{\hbar^4}\cdot\frac{4\pi}{(\alpha m)^2\,\bigl[(\alpha m)^2+4p^2\bigr]}.

The integrand is $2\pi\sin\theta$ times the differential cross section $d\sigma/d\Omega=|f(\theta)|^2$ of the Yukawa potential in the Born approximation, so the left side is the total cross section $\sigma=\int\frac{d\sigma}{d\Omega}\,d\Omega$ computed in the section Cross section.

Formalization Note The integral is the interval integral over $[0,\pi]$ . No sign conditions on $\mu,\hbar,p$ are imposed (the identity is valid for all real values; for $\hbar=0$ both sides are $0$ by Lean's division convention).

Preamble

import Mathlib
import Definitions.Def_YukawaPotential_Defs

open MeasureTheory Filter Topology

Formal statement

namespace YukawaPotential
theorem yukawa_total_cross_section (μ ℏ g α m p : ℝ) (hα : 0 < α) (hm : 0 < m) :
    ∫ θ in (0 : ℝ)..Real.pi,
        4 * μ ^ 2 * g ^ 4 / ℏ ^ 4 *
          (2 * Real.pi * Real.sin θ / ((α * m) ^ 2 + 4 * p ^ 2 * Real.sin (θ / 2) ^ 2) ^ 2) =
      4 * μ ^ 2 * g ^ 4 / ℏ ^ 4 * (4 * Real.pi / ((α * m) ^ 2 * ((α * m) ^ 2 + 4 * 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': σ = ∫ dσ/dΩ dΩ = (4μ²g⁴/ħ⁴) ∫_0^π 2π sin θ dθ / [(αm)² + 4p² sin²(θ/2)]² = (4μ²g⁴/ħ⁴) · 4π/((αm)²[(αm)² + 4p²]).

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,p$ (arbitrary) and real numbers $\alpha>0$ , $m>0$ . Write $C = 4\mu^2g^4/\hbar^4$ (equal to $0$ when $\hbar=0$ , by the division convention). The statement asserts

\int_0^\pi C\cdot\frac{2\pi\sin\theta}{\bigl((\alpha m)^2+4p^2\sin^2(\theta/2)\bigr)^2}\,d\theta \;=\; C\cdot\frac{4\pi}{(\alpha m)^2\bigl((\alpha m)^2+4p^2\bigr)},

where the left side is the integral over the interval from $0$ to $\pi$ (a Lebesgue integral over $(0,\pi]$ , defaulting to $0$ if not integrable). The case $p=0$ is included.

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