Yukawa shell theorem, exterior: a shell acts as a point source of strength $G\,\sinh(\alpha mR)/(\alpha mR)$

Proved

YukawaPotential.yukawaShellPotential_exterior

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

mathematical-physicsyukawa-potential

Let $G,g\in\mathbb R$ , $\alpha>0$ , $m>0$ , $R>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 $|x|>R$ ,

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

So outside the shell its potential equals that of a point source at the centre with magnitude $G\,\frac{\sinh \alpha mR}{\alpha mR}$ , which is larger than $G$ .

Preamble

import Mathlib
import Definitions.Def_YukawaPotential_Defs

open MeasureTheory Filter Topology

Formal statement

namespace YukawaPotential
theorem yukawaShellPotential_exterior (G g α m R : ℝ) (hα : 0 < α) (hm : 0 < m) (hR : 0 < R)
    (x : EuclideanSpace ℝ (Fin 3)) (hx : R < ‖x‖) :
    yukawaShellPotential G g α m R x =
      G * g * (Real.exp (-(α * m * ‖x‖)) / ‖x‖) * (Real.sinh (α * m * R) / (α * m * R)) := 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': 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$ , $R>0$ , and a point $x\in\mathbb R^3$ with $|x|>R$ . Let

S(x) = G\,g\,\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 in $\mathbb R^3$ and $\sigma$ is the rotation-invariant surface measure on it obtained from Lebesgue measure by the cone construction (total mass $4\pi$ ), the integral being a Bochner integral (defaulting to $0$ if not integrable). The statement asserts

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

Points with $|x|\le 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

Yukawa shell theorem, exterior: a shell acts as a point source of strength G sinh⁡(αmR)/(αmR)G\,\sinh(\alpha mR)/(\alpha mR)Gsinh(αmR)/(αmR)

Yukawa shell theorem, exterior: a shell acts as a point source of strength $G\,\sinh(\alpha mR)/(\alpha mR)$