An independent reproduction of two computer-assisted strong-coupling SU(2) lattice mass-gap certificates

This technical note is an independent computational audit of two recent, unrefereed Zenodo records on the strong-coupling mass gap of four-dimensional SU(2) lattice Yang–Mills theory: H. T. Rajabu (doi:10.5281/zenodo.23691339) and D. Bhattacharjee, U. Bhattacharya, J. M. Lockwood and T. Romanov (doi:10.5281/zenodo.23992883, v4.37.0). All three of Rajabu’s verification scripts pass on a fresh run (1144, 387 and 168 checks), and their output matches the archived files apart from run times. For Bhattacharjee et al., the ball-arithmetic certificate for SU(2) plaquette blocks reproduces the computed bound α(0.351) ≤ 0.99995; at β_W = 0.3511 the computed bound exceeds 1, as the authors state. The core-only Lean 4 files accept the encoded propositions, and a negative control with one inflated constant is rejected. Separately, a discretised optimal-transport computation, sampled at ten field strengths and seven directions including non-zonal ones, is consistent with the single-link Wasserstein constant 1/4 and hence with the single-link threshold β_W < 2/9. This is numerical corroboration, not a proof. The note keeps apart computational reproduction, Lean verification of encoded propositions, and validation of the complete mathematical arguments. It does not attempt the last, claims no new theorem, and does not concern the continuum limit or the Clay Millennium problem. The record contains the note, the scripts written for it (w1_vmf.py, dob.py) and the console output of every run; README.md lists all 22 files. Computations and drafting were assisted by an AI system (Claude, Anthropic).