Yukawa potential solves the screened Poisson equation $\Delta\phi=(\alpha m)^2\phi$ away from the origin

Proved

YukawaPotential.yukawaPotential_laplacian

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

mathematical-physicsyukawa-potential

Let $g,\alpha,m\in\mathbb R$ and consider the potential of a point source at the origin of $\mathbb R^3$ ,

\phi(x) = V(|x|) = -g^2\,\frac{e^{-\alpha m |x|}}{|x|}.

Then at every point $x\neq0$ ,

\Delta\phi(x) = (\alpha m)^2\,\phi(x),

where $\Delta=\partial_1^2+\partial_2^2+\partial_3^2$ is the Laplacian on $\mathbb R^3$ .

This is the static, radial form $\nabla^2\phi=\mu^2\phi$ of the massive wave equation $\Box\phi+\mu^2\phi=0$ from the section Relation to wave equation, whose radial solutions are $\phi(r)=K e^{-\mu r}/r$ ; here $K=-g^2$ and $\mu=\alpha m$ .

Formalization Note The Laplacian is Mathlib's Laplacian.laplacian on the inner-product space EuclideanSpace ℝ (Fin 3) (trace of the second Fréchet derivative). No sign condition on $\alpha m$ is needed.

Preamble

import Mathlib
import Definitions.Def_YukawaPotential_Defs

open MeasureTheory Filter Topology

Formal statement

namespace YukawaPotential
theorem yukawaPotential_laplacian (g α m : ℝ) (x : EuclideanSpace ℝ (Fin 3)) (hx : x ≠ 0) :
    Laplacian.laplacian (fun y : EuclideanSpace ℝ (Fin 3) => yukawaPotential g α m ‖y‖) x =
      (α * m) ^ 2 * yukawaPotential g α 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 'Relation to wave equation': □φ + μ²φ = 0; for radial time-independent φ, ∇²φ = μ²φ, with solutions φ(r) = K e^{-μr}/r, 'which is the Yukawa potential'.

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 arbitrary real numbers $g,\alpha,m$ (no sign conditions) and a point $x\in\mathbb R^3$ with $x\neq0$ . Let $\phi:\mathbb R^3\to\mathbb R$ be $\phi(y) = -g^2 e^{-\alpha m |y|}/|y|$ (Euclidean norm; $\phi(0)=0$ by the division convention). The statement asserts

(\Delta\phi)(x) = (\alpha m)^2\,\phi(x),

where $\Delta\phi(x)$ is the Laplacian of $\phi$ at $x$ , defined as the trace (with respect to the Euclidean inner product) of the second Fréchet derivative of $\phi$ at $x$ , i.e. $\sum_{i=1}^3 \partial_i^2\phi(x)$ ; if $\phi$ were not twice differentiable at $x$ this quantity would default to $0$ . Nothing is claimed at $x=0$ .

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 potential solves the screened Poisson equation Δϕ=(αm)2ϕ\Delta\phi=(\alpha m)^2\phiΔϕ=(αm)2ϕ away from the origin

Yukawa potential solves the screened Poisson equation $\Delta\phi=(\alpha m)^2\phi$ away from the origin