# AI provenance: Mass Gap of Lattice Yang–Mills Theory up to the Dobrushin Ceiling

Authors: Deep Bhattacharjee (corresponding author, ORCID 0000-0003-0466-750X;
formerly EGSPL, Bhubaneswar, Odisha 751030, India, and formerly University of
Calcutta, Senate House, 87/1 College Street, Kolkata 700073, West Bengal,
India) and Ushashi Bhattacharya (ORCID 0009-0002-2254-3914; formerly National
Taiwan University, Taipei 106319, Taiwan).

- Paper: https://github.com/creelie/4Y-M/blob/main/preprintYangMillsDobrushinCeiling/YangMillsDobrushinCeiling.pdf
- Lean certificate and checks: https://github.com/creelie/4Y-M (Zenodo record https://doi.org/10.5281/zenodo.23444338, with later versions)

## Result

For four-dimensional lattice SU(2) Yang–Mills theory with Wilson coupling
β_W < 2/9 the infinite-volume Gibbs measure is unique, truncated correlations
decay exponentially, and the transfer matrix has a spectral gap
m ≥ −log(9β_W/2). The value 2/9 is the ceiling of every single-link
Wasserstein–Dobrushin argument, so the result is best possible for this
method. The key new statement is the sharp quarter: for every von
Mises–Fisher law on the three-sphere and every unit vector h, the covariance
of a chordally 1-Lipschitz function with ⟨h, x⟩ is at most 1/4, so that
W₁(ν_b, ν_b′) ≤ |b − b′|/4, with equality at b = 0; the constant fails in the
geodesic metric. The paper also proves the sharp Hessian bound 4d, the
curvature regime |β| < 1/(8d) for SU(N) with its limit, uniqueness on the whole
curvature range, and a gauge-invariant finite-box criterion.

## Who did what

Deep Bhattacharjee chose the problem, directed the work, set the format and
the journal style, and ran the computations. Claude (Anthropic), used through
Claude Code under his direction, produced the following:

- the proof of the sharp quarter and the revisions of Theorems E and F;
- the Lean 4 formalisation of the finite and algebraic steps;
- the Python check script;
- the figures;
- the LaTeX text, its footnotes and appendices, and the reference list (every
  reference, the seven self-citations included, was checked against the
  publisher's or Crossref's record);
- this file and the submission notes.

No other AI system took part.

## How the result is checked

- **Lean 4.33.0 with Mathlib.** `YangMills/StrongCoupling/QxCoefficients.lean`
  proves the closed form and the nonnegativity of every Taylor coefficient of
  the function 𝒟 that controls the transverse part; `ZonalBound.lean` proves
  the rational identities, the sign of the cubic, the Riccati barrier
  derivative and the final zonal inequality; `Thresholds.lean` proves the
  Dobrushin row sum and the thresholds of Theorems E and F. All 25 theorems
  depend only on propext, Classical.choice and Quot.sound, with no `sorry`
  or added axiom, and `lake build` passes.
- **Independent check.** `strong-coupling/prd/checks/quarter/check_quarter.py`
  verifies the coefficient formula in exact arithmetic, the Bessel sums and
  both parts of the norm at 50 digits, the third Riccati barrier and the
  factorisation of the zonal majorant (49 checks).

## What is not claimed

The Bessel identities, the harmonic extension and the Riccati comparison are
proved by hand and are not formalised in Lean. The result is about lattice
gauge theory at a fixed lattice spacing. It does not prove the existence of
continuum Yang–Mills theory or its mass gap (the Clay Millennium problem); the
paper lists the remaining gaps: intermediate fixed coupling, the crossover to
Bałaban's weak-coupling regime, the continuum limit and a gap in physical
units. A search of arXiv and the journal literature up to October 2026 found
no published proof of the sharp quarter. A 2026 preprint attributed to
J. Lockwood, seen only as an abstract, announces uniqueness for
four-dimensional SU(2) at β_W < 2/9 by a Wasserstein–Dobrushin argument; its
proof could not be checked, and the paper cites it in a footnote.