Yukawa potential and the potential of a uniform spherical shell

Definition

YukawaPotential_Defs

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

mathematical-physicsyukawa-potential

Two definitions used throughout the mission.

Yukawa potential. For real parameters $g$ (coupling), $\alpha$ (scaling constant), $m$ (mass) and a radial distance $r$ ,

V_{g,\alpha,m}(r) = -g^2\,\frac{e^{-\alpha m r}}{r}.

Potential of a uniform spherical shell. For a thin uniform shell of radius $R$ centred at the origin with total scaling constant $G$ , the potential at $x\in\mathbb R^3$ felt by a point of scaling constant $g$ is $G g$ times the average, over the unit sphere $S^2$ with its uniform surface measure $\sigma$ , of the pair interaction:

V^{\mathrm{shell}}_{G,g,\alpha,m,R}(x) = G\,g\;\frac{1}{\sigma(S^2)}\int_{S^2}\frac{e^{-\alpha m\,|x-Ru|}}{|x-Ru|}\,d\sigma(u).

These are the objects of the article's introduction and of its section Spherical shell.

Formalization Note Lean's division by zero returns $0$ , so $V(0)=0$ and the shell integrand is $0$ at a point $u$ with $x=Ru$ ; statements about these objects restrict to $r>0$ , $x\ne0$ , or $|x|\neq R$ as appropriate. The surface measure is Mathlib's Measure.toSphere of Lebesgue measure; the definition uses the normalised average ⨍.

Definition code

import Mathlib

namespace YukawaPotential

open MeasureTheory

/-- The Yukawa (screened Coulomb) potential
`V(r) = -g^2 * exp(-α m r) / r`, with coupling `g`, scaling constant `α`,
mass `m` and radial distance `r`. -/
noncomputable def yukawaPotential (g α m r : ℝ) : ℝ :=
  -g ^ 2 * Real.exp (-(α * m * r)) / r

/-- Potential at the point `x ∈ ℝ³` felt by a point of scaling constant `g`, produced by an
infinitesimally thin uniform spherical shell of radius `R` centred at the origin with total
scaling constant `G`, where each pair interacts through `G g exp(-α m d) / d` at distance `d`:
`G g` times the average of `exp(-α m ‖x - R u‖) / ‖x - R u‖` over the unit sphere `u ∈ S²`
(with respect to the uniform surface measure). -/
noncomputable def yukawaShellPotential (G g α m R : ℝ) (x : EuclideanSpace ℝ (Fin 3)) : ℝ :=
  G * g * ⨍ u : Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1,
    Real.exp (-(α * m * ‖x - R • (u : EuclideanSpace ℝ (Fin 3))‖)) /
      ‖x - R • (u : EuclideanSpace ℝ (Fin 3))‖ ∂(volume.toSphere)

end YukawaPotential

Source

Wikipedia, "Yukawa potential", revision oldid=1371658231, https://en.wikipedia.org/w/index.php?title=Yukawa_potential&oldid=1371658231, introduction (definition of V_Yukawa) and section 'Spherical shell'.

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.

The file declares two real-valued functions inside the namespace YukawaPotential.

First function. For any four real numbers $g,\alpha,m,r$ it returns

V(g,\alpha,m,r) = \frac{-g^2\cdot e^{-(\alpha m r)}}{r}.

No restriction is placed on any argument: $g,\alpha,m$ may be negative or zero, and $r$ may be zero or negative. At $r=0$ the value is $0$ , because division by zero is defined to return $0$ . For $r<0$ the formula is evaluated literally.

Second function. For real numbers $G,g,\alpha,m,R$ and a point $x$ of three-dimensional Euclidean space $\mathbb R^3$ , it returns

G\cdot g\cdot \frac{1}{\sigma(S^2)}\int_{S^2} \frac{e^{-(\alpha m\,|x-Ru|)}}{|x-Ru|}\,d\sigma(u),

where $S^2$ is the unit sphere $\{u\in\mathbb R^3 : |u|=1\}$ , $|\cdot|$ the Euclidean norm, and $\sigma$ the measure on $S^2$ obtained from Lebesgue measure on $\mathbb R^3$ by the cone construction (the measure of a set $A\subseteq S^2$ is $3$ times the Lebesgue volume of $\{tu : 0<t<1,\ u\in A\}$ ); this is a rotation-invariant measure of total mass $4\pi$ . The integral is a Bochner integral divided by the total mass (an average). If the integrand is not integrable, the integral is defined to be $0$ . When $x=Ru$ for some $u$ the integrand at that $u$ is $0$ by the division convention. No restriction is placed on $R$ (it may be zero or negative), nor on $\alpha$ , $m$ , $G$ , $g$ .

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