An area law for four-dimensional SU(2) lattice gauge theory up to β ≈ 0.813

An area law for four-dimensional SU(2) lattice gauge theory up to β ≈ 0.813 (note v1.0, 1 November 2026). Result. Consider the SU(2) Wilson lattice gauge theory on the periodic torus (Z/LZ)4, L ≥ 3, with weight exp(−β Σp(1 − ½ Re Tr Up)). For 0 ≤ β ≤ 0.81348, every planar rectangular Wilson loop with sides R ≤ L/2 and T ≤ L−1 satisfies |⟨W⟩| ≤ CT θRT, with explicit constants θ = 1 − 7.054×10−6 and C = 5.639×105 independent of L and of β; in particular the string tension (defined with R → ∞) is positive. With a larger certificate (memory 13, 4.4 GB, not supplied but identified by its SHA-256) the same argument gives β ≤ 0.81498; this is stated as a remark only. Method. The proof follows the method of Borgs and Seiler (1983, Appendix B): the slab decomposition of Durhuus and Fröhlich, a random-walk expansion of the slab σ-models and the positivity of the transfer matrix, which yields the range β < 12/17 ≈ 0.7059. It is refined in two ways. (I) The ratio of slab partition functions is controlled by a strict operator inequality, where the constant comes from the Peter–Weyl spectrum (the spin-0 mode is extremal), followed by a site-by-site Cauchy–Schwarz factorisation. (II) The resulting weighted walks are counted with a memory of 11 steps, through a transfer matrix on 7 821 056 symmetry classes whose spectral radius is bounded by an integer Perron certificate (the 125 MB file attached to this record). Every numerical inequality of the proof is verified in exact integer or rational arithmetic, and the certificate is re-verified by two further programs, one of them written separately for an adversarial verification. What is new and what is not. To our knowledge, the widest explicit confinement range already published for the SU(2) Wilson theory in four dimensions is β < 12/17 (Borgs and Seiler, Commun. Math. Phys. 91 (1983) 329, eq. (II.55) and Appendix B), stated for correlations of Polyakov loops at every temperature and every magnetic coupling; the authors do not state a bound for each rectangular loop. This note refines the threshold of the Borgs–Seiler method from 12/17 to 0.81348 (+15.2%), with bounds for each rectangle on tori. It is not an independent method, and no priority is claimed beyond this refinement. Tomboulis (arXiv:0707.2179) claims confinement for all values of the coupling in an unpublished preprint, whose argument Ito and Seiler (arXiv:0803.3019) discuss as having gaps; it is not counted here as an established range. The value 0.81348 lies between the estimate 4/5 announced without proof by Fröhlich (1980), in the reading discussed in the note, and the value 0.8222 given by a non-backtracking heuristic. Status. Computer-assisted. The analytic part is proved on paper; its numerical inputs are verified by programs in exact arithmetic and re-verified by other programs. The proof and the certificates have been checked by machine only (independent programs and adversarial reviews carried out by language models). They have not been read by a human referee. A Lean 4 formalisation covers the combinatorial part, the certificate checker and the final arithmetic (proved in the Lean kernel and accepted by a second, independent kernel) and the memory-11 certificate (checked by compiled execution); the analytic reduction, the monotonicity lemma and the certified bounds on the weights are assumed there. Limitations. Tori only (the factor per site uses exactly six links per site, the trace formula uses periodicity); in infinite volume only the weak limit points of torus measures are covered. Planar rectangular loops only; the string tension obtained near the threshold is tiny (7×10−6), and the bound is non-trivial only for R above about 1.9×106 at β*. Strong coupling only: nothing is claimed about the continuum limit or the Yang–Mills mass gap. The literature search is not exhaustive: not consulted are Seiler’s Lecture Notes in Physics 159 (1982), Brydges–Giffen–Durhuus–Fröhlich (1986) beyond its abstract, and Guerra–Immirzi–Marra (1978), known only through Borgs–Seiler; MathSciNet and zbMATH were not queried and no specialist was consulted. Contents of this record. (1) The note (PDF). (2) A zip archive of the GitHub folder papers/Paper_AreaLaw_SU2_4D at tag v7.8.0: the note in LaTeX, the programs of the proof, the weights, the outputs, the independent checks, the Lean 4 project (sources and logs) and the memory-11 certificate compressed with xz (certificat_h_m11_J40674_100000.bin.xz, 8 780 360 bytes, SHA-256 776f4f27be0aabb32ec81050883448b4004db11289b2a1cf338614e188bbc1e4); its README explains the reproduction. (3) The memory-11 certificate itself, certificat_h_m11_J40674_100000.bin (125 136 920 bytes, SHA-256 b50d3769b0ea17d1da13f4e870a7786407192a9885ecceb390ef18cde50cf142), which is too large for GitHub as a raw file. The certificate can be unpacked from the .xz file or regenerated byte for byte from the programs of the archive, and checked by its fingerprint and by the program verif_cert. Prepared with the assistance of AI models (Claude Opus 5.5, Anthropic; Kimi K3.1 Pro, Moonshot AI; DeepSeek V4 Pro, DeepSeek), whose roles are described in the section “Use of AI” of the note.