Yukawa shell theorem, interior potential

Proved

YukawaPotential.yukawaShellPotential_interior

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

mathematical-physicsyukawa-potential

Let $G,g\in\mathbb R$ , $\alpha>0$ , $m>0$ , and let $V^{\mathrm{shell}}$ be the potential of a uniform thin spherical shell of radius $R$ and total scaling constant $G$ centred at the origin, felt by a point of scaling constant $g$ (see the definition item). For every $x\in\mathbb R^3$ with $0<|x|<R$ ,

V^{\mathrm{shell}}(x) = G\,g\,\frac{e^{-\alpha m R}}{R}\cdot\frac{\sinh(\alpha m |x|)}{\alpha m |x|}.

Unlike the Newtonian case, the interior potential is not constant.

Formalization Note The centre $x=0$ is excluded because the article's formula is there only defined as a limit ( $\sinh(\alpha m r)/(\alpha m r)\to1$ ), while Lean would evaluate $\sinh(0)/0$ to $0$ . The hypotheses force $R>0$ .

Preamble

import Mathlib
import Definitions.Def_YukawaPotential_Defs

open MeasureTheory Filter Topology

Formal statement

namespace YukawaPotential
theorem yukawaShellPotential_interior (G g α m R : ℝ) (hα : 0 < α) (hm : 0 < m)
    (x : EuclideanSpace ℝ (Fin 3)) (hx0 : 0 < ‖x‖) (hx : ‖x‖ < R) :
    yukawaShellPotential G g α m R x =
      G * g * (Real.exp (-(α * m * R)) / R) * (Real.sinh (α * m * ‖x‖) / (α * m * ‖x‖)) := by sorry
end YukawaPotential

Source

Wikipedia, "Yukawa potential", revision oldid=1371658231, https://en.wikipedia.org/w/index.php?title=Yukawa_potential&oldid=1371658231, section 'Spherical shell': the interior potential is V(r < R) = G g (e^{-αmR}/R) (sinh αmr)/(αmr).

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 $G,g$ (arbitrary), real numbers $\alpha>0$ , $m>0$ , a real number $R$ , and a point $x\in\mathbb R^3$ with $0<|x|<R$ (so $R>0$ ). Let

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

with $S^2$ the unit sphere in $\mathbb R^3$ and $\sigma$ its rotation-invariant surface measure from the cone construction (total mass $4\pi$ ); the integral is a Bochner integral (defaulting to $0$ if not integrable). The statement asserts

S(x) = G\,g\cdot\frac{e^{-\alpha m R}}{R}\cdot\frac{\sinh(\alpha m|x|)}{\alpha m|x|}.

The centre $x=0$ and the points with $|x|\ge R$ are not covered.

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