Consistency of Potential‑Model and Dispersion‑Relation Approaches to the Charmonium Fine‑Structure Splitting: A Formal Verification

We present a formal algebraic verification, carried out in the Lean 4 proof assistant with the Mathlib library, of the consistency between two theoretical approaches to the charmonium fine‑structure splitting ΔM = M (ψ (2S) ) − M (J/ψ). The first approach uses the potential‑model expansion (Coulomb + linear confinement + spin‑spin + hadronic shift) ; the second uses a dispersion relation derived from NRQCD and the optical theorem. We prove that the coefficient of the leading non‑perturbative (hadronic) correction matches exactly between the two descriptions, once the coupling constants are identified via the Van Royen–Weisskopf relation through the Coulomb wavefunction at the origin. The discrepancy is identically zero. The Coulomb contribution is computed analytically as ΔECoulomb = (3/8) mc αₛ² = 47. 25 MeV for mc = 1. 4 GeV, αₛ = 0. 3. Adding confinement (≈529 MeV) and the spin‑spin correction, the total (≈576 MeV) is within 2% of the experimental value 589. 20 MeV. The Lean source code is provided as supplementary material.