# AI provenance: Mass Gap of Four-Dimensional Lattice Yang--Mills Theory in a Forest Gauge

Authors: Deep Bhattacharjee and Ushashi Bhattacharya. No AI system is an author or contributor.

## How the work was produced

Deep Bhattacharjee chose the problem, directed the work and ran the computations. Claude (Anthropic), used through Claude Code under his direction, produced the proofs, the Lean 4 file, the programs, the figures and the LaTeX text, which the authors reviewed. The Anaxia engine of the BLLM system (eBLLM release v3.0.5, https://github.com/creelie/eBLLM/releases/tag/v3.0.5) first assembled the SU(2) composite; release v3.1.0 (https://github.com/creelie/eBLLM/releases/tag/v3.1.0) records the Yang-Mills runs in its failure log and supplied no step of the proofs. The plaquette blocks, their SU(3) version and their constants were found and checked without the engine.

## How the results are checked

Lean 4 with Mathlib proves the combinatorics of the line field by decide (seven theorems, propext at most). The local Hessian blocks are checked in exact rationals. The SU(3) bounds are certified in ball arithmetic (Arb through python-flint) on 2341 boxes at r = 3/2 and 1063 boxes at r = 38/25; the plaquette-block constants are certified on 841 and 784 boxes.

## What is not claimed

The results hold at fixed lattice spacing. They do not prove the existence of continuum Yang-Mills theory or its mass gap (the Clay Millennium problem). The proofs are written by hand and have not yet been refereed.

## Labels given on the Hexagon form

- Text of the contribution: a mix of human-written and AI-generated (to be confirmed by the authors).
- Human understanding at submission: some parts, but not all, checked and understood by a human (to be confirmed by the authors).

## Where everything is

Release v3.4.0: https://github.com/creelie/4y-m/releases/tag/v3.4.0.