Dobrushin uniqueness for the four-dimensional SU(2) Wilson lattice gauge measure for beta < 2/9, with interval/Lean certificates (note v1.4)

Dobrushin uniqueness for the four-dimensional SU(2) Wilson lattice gauge measure for β < 2/9, with interval/Lean certificates (note v1.4, 28 October 2026; v1.4 is a literature update of v1.3, which was not publicly released). Result. For the SU(2) Wilson action on Z4 with weight exp(−β Σp(1 − ½ Re Tr Up)), the Gibbs (DLR) measure is unique for 0 ≤ β < 2/9 ≈ 0.222 (equivalently g2 > 18; βtH < 1/18 in the 't Hooft normalisation). Method: Dobrushin's criterion in its Wasserstein (W1) form with the Euclidean (chordal) metric of R4 on SU(2) ≅ S3, the metric used by Levin (1980). The one-site coefficient in a field of strength κ ≤ 4/3 is shown to equal Eκ[x⊥2] ≤ 1/4 − 0.0084κ2, maximal at zero field; each of the 18 neighbouring links has influence exactly β/4 and the Dobrushin sum is 9β/2. This confirms, for N = 4 and |g| ≤ 4/3, the maximum-at-zero-field property conjectured by Levin (CMP 78, 1980, Remark 3.7), which Bhattacharjee and Bhattacharya prove for N = 4 and all fields (Theorem 7 of the preprint cited below). Secondary result: with the geodesic metric the exact coefficient is 8β/(9π), which gives the weaker range β < π/16 (the main result of v1.2). Each threshold is sharp for its criterion. Status. The chordal one-link identity is proved on paper (divergence-free field bound, explicit field, analytic elimination of the direction) up to a one-variable inequality on [0, 4/3], which is interval-certified with Arb/python-flint (256 boxes) and independently recertified with mpmath interval arithmetic and exact rationals; its final rational step and the threshold arithmetic are checked in Lean 4 (Mathlib v4.34.0; axioms propext, Classical.choice, Quot.sound only). The archive contains the note (PDF and LaTeX), both certificates with reproduction scripts, both independent checks, and a standalone Lean project that builds from scratch. Limitations. Uniqueness only (no decay of correlations, spectral gap or log-Sobolev inequality is claimed). The mathematical reductions are proved on paper but not formalised; the certificates have not been audited outside the project. Prior art: Levin (1980), Royer (1986), Gross (1979) and Simon (1979) were read; none mentions gauge theories or states β < π/16 or better. Not consulted: Seiler's monograph (LNP 159), the content of Georgii's book, and Simon's book on lattice gases. A strong-coupling statement: nothing is claimed about the continuum limit or the Yang–Mills mass gap. Prepared with the assistance of Claude (Opus 5.5, Anthropic); every claim in the note carries a status label. Prior public statement. the uniqueness range beta < 2/9 for the four-dimensional SU(2) model (with exponential decay and a lattice mass gap) and the all-field bound W1(nu_b, nu_b') ≤ |b - b'|/4 on S^3 were stated publicly, with proofs, in the preprint of D. Bhattacharjee and U. Bhattacharya, "Mass Gap of Lattice Yang-Mills Theory up to the Dobrushin Ceiling", hexagon:2610.00341v1, 18 October 2026 (Theorems E, F and 7). This note was prepared independently and makes no priority claim. Its own contributions: the exact one-link chordal coefficient E_kappa[x_perp^2] for kappa ≤ 4/3 with an explicit remainder, the exact geodesic coefficient 8 beta/(9 pi), two independent interval-arithmetic certificates, Lean-checked final steps, and explicit transfers of the published constants of Levin, Royer, Gross, Simon and Shen-Zhu-Zhu to the Wilson link.