Deep Bhattacharjee (corresponding author, head of the project), Ushashi Bhattacharya, James Montgomery Lockwood, Tristan Romanov, Ikailo John Sessford, Sanjeevan Singha Roy.
15 November progress: error-stable ascent, continuum-interface audit, and precise remaining estimate. Six new Lean declarations extend the ascent to quantified approximation errors. Written interface lemmas accommodate the external construction's sparse mesh sequence and phase decomposition. The unconditional weak-coupling mass gap remains open.
| Proved | Open |
|---|---|
| Mass gap of 4D lattice Yang–Mills theory at strong coupling, every compact simple group, explicit bounds | The one-scale bound at weak coupling |
| Theorem F: a compatible Wightman limit on tori and one bound on partition functions at one scale give the continuum mass gap and a unique vacuum | A complete checked adapter to the selected construction, and the bound at its actual couplings |
| The one bound is a lattice gap plus a Stefan–Boltzmann bound on the thermal free energy, and it forces a vanishing centre-vortex free energy | The lattice gap at weak coupling |
| The gap alone does not give the count of states; the centre vortex controls only the charged states | The glueball gap and the count of states at weak coupling |
| The unrenormalised loop variables have a trivial limit | The Clay problem |
| Folder | Contents | Run |
|---|---|---|
YangMills/ | Lean 4 project over Mathlib | lake exe cache get && lake build |
scripts/ | axiom audit | lake env lean scripts/Axioms.lean |
julia/ | constants of the paper | julia julia/constants.jl |
research/2026-11-15/ | proof progress and explicit remaining assumptions | python scripts/check_closure_progress.py |
The external construction assessment reports a Wilson scaling-limit Wightman theory and explicitly leaves the mass gap unproved. Our source audit addresses particular compatibility conditions; it does not claim to have rebuilt that entire construction.