Construction of four-dimensional quantum Yang–Mills theory, with a conditional mass gap, and a formal companion in Lean

We construct four-dimensional quantum Yang-Mills theory from Balaban's renormalization group with two estimates taken as named inputs, and we prove its mass gap under one hypothesis, which we reduce to a bound on one physical box that is not proved here. For every compact simple gauge group the theory is obtained as a limit of Wilson's lattice gauge theory along a single refining family of lattice spacings and bare couplings. Uniform bounds on the connected cumulants of renormalized local sources give Euclidean Schwinger distributions with temperedness, reflection positivity, symmetry, translation invariance and hypercubic covariance, and the Hilbert space, positive Hamiltonian and momentum operators of the reconstruction. The scalar curvature density obeys the short-distance law predicted by asymptotic freedom, and the theory is not free. The operator product expansion and the Ward identities of a calibrated stress tensor are proved from the two named inputs. The mass gap is proved under one hypothesis, the long-time decay of the cutoff correlations at a common physical rate; we prove that the hypothesis is equivalent to a positive spectral gap of the Hamiltonian and that it follows from a free-energy bound on one fixed physical box. Under the hypothesis the scalar sector is Euclidean covariant, its Wightman theory is reconstructed with a unique vacuum, and the Hamiltonian has spectrum in {0} and [m, infinity). The proof is accompanied, result by result, by a formal development in Lean 4 with Mathlib. 344 pages. Files: the paper (PDF), its TeX source, and the Lean 4 sources of the formal companion (1077 files).