Prove2Me

Massless Yukawa potential is the Coulomb potential

Proved
YukawaPotential.yukawaPotential_massless_eq_coulomb

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

mathematical-physicsyukawa-potential

For all real gg, α\alpha and rr, the Yukawa potential with mass m=0m=0 is the Coulomb potential:

Vg,α,0(r)=−g2 1r.V_{g,\alpha,0}(r) = -g^2\,\frac{1}{r}.

This is the article's observation that for a massless exchange particle e−αmr=e0=1e^{-\alpha m r}=e^0=1, so the Yukawa potential reduces to VCoulomb(r)=−g21rV_{\mathrm{Coulomb}}(r)=-g^2\frac1r.

Formalization Note The identity holds for every real rr, including r=0r=0 where both sides equal 00 by Lean's division convention.

Preamble
import Mathlib
import Definitions.Def_YukawaPotential_Defs

open MeasureTheory Filter Topology
Formal statement
namespace YukawaPotential
theorem yukawaPotential_massless_eq_coulomb (g α r : ℝ) :
    yukawaPotential g α 0 r = -g ^ 2 * (1 / 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 'Relation to Coulomb potential': m = 0 ⇒ e^{-αmr} = e^0 = 1, so V_Yukawa simplifies to V_Coulomb(r) = -g² (1/r).
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.

For every real gg, α\alpha and rr (no hypotheses), with V(g,α,m,r)=−g2e−αmr/rV(g,\alpha,m,r) = -g^2 e^{-\alpha m r}/r, the statement asserts

V(g,α,0,r)=−g2⋅1r.V(g,\alpha,0,r) = -g^2\cdot\frac{1}{r}.

This includes r=0r=0 (both sides are 00 by the division-by-zero convention) and negative rr; α\alpha is arbitrary, including 00 and negative values.

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