We present a formal verification, carried out in the Lean 4 proof assistant, of the consistency between the potential-model and dispersion-relation approaches to the hadronic correction in the Υ (2S) –Υ (1S) mass splitting of bottomonium. The coefficient of the leading non-perturbative (hadronic) correction is shown to be identical in both frameworks, as an exact algebraic identity independent of the coupling constant, the wavefunction at the origin, and the hadronic spectral integral. Numerical evaluation with standard parameters (mb = 4. 18 GeV, αₛ (mb) = 0. 18, σ = 0. 18 GeV²) yields a total splitting consistent with the experimental value ΔMₑxp = 563. 9 MeV.
Yuri N. Berdinsky (Thu,) studied this question.