Yukawa potential is negative and strictly increasing on $(0,\infty)$

Proved

YukawaPotential.yukawaPotential_neg_and_strictMonoOn

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

mathematical-physicsyukawa-potential

Let $g\neq 0$ , $\alpha>0$ and $m\ge 0$ , and let $V(r)=-g^2 e^{-\alpha m r}/r$ be the Yukawa potential. Then

$V(r)<0$ for every $r>0$ , and
$V$ is strictly increasing on $(0,\infty)$ :

0<r_1<r_2 \implies V(r_1)<V(r_2).

This is the article's statement that "the potential is monotonically increasing in $r$ and it is negative, implying the force is attractive".

Formalization Note The hypothesis $g\neq0$ excludes the identically zero potential; $\alpha>0$ and $m\ge0$ are the physical conventions on the scaling constant and the mass.

Preamble

import Mathlib
import Definitions.Def_YukawaPotential_Defs

open MeasureTheory Filter Topology

Formal statement

namespace YukawaPotential
theorem yukawaPotential_neg_and_strictMonoOn (g α m : ℝ) (hg : g ≠ 0) (hα : 0 < α) (hm : 0 ≤ m) :
    (∀ r : ℝ, 0 < r → yukawaPotential g α m r < 0) ∧
      StrictMonoOn (yukawaPotential g α m) (Set.Ioi 0) := by sorry
end YukawaPotential

Source

Wikipedia, "Yukawa potential", revision oldid=1371658231, https://en.wikipedia.org/w/index.php?title=Yukawa_potential&oldid=1371658231, introduction (first paragraph): 'The potential is monotonically increasing in r and it is negative'.

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,\alpha,m$ with $g\neq0$ , $\alpha>0$ and $m\ge0$ . Write $V(r) = -g^2 e^{-\alpha m r}/r$ for real $r$ (with $V(0)=0$ by the division-by-zero convention). The statement asserts the conjunction of:

for every real $r>0$ , $V(r)<0$ (strict inequality);
$V$ is strictly increasing on the open interval $(0,\infty)$ : for all $r_1,r_2$ with $0<r_1<r_2$ , $V(r_1)<V(r_2)$ .

Nothing is claimed for $r\le 0$ . The case $m=0$ is included (then $V(r)=-g^2/r$ ).

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 is negative and strictly increasing on (0,∞)(0,\infty)(0,∞)

Yukawa potential is negative and strictly increasing on $(0,\infty)$