No lattice tiling of Z^35 or Z^805 by Lee balls of radius three: paper, Lean 4 formalization and verification code

We prove that there is no lattice tiling of Z^35 or of Z^805 by Lee balls of radius three. A. Xiao and Y. Zhou (arXiv:2610.19775, Theorem 5.1) decided the lattice Golomb-Welch conjecture for every pair (n, r) with n >= 3, r >= 2 and fewer than 2^30 points in the ball, except (35, 3) and (805, 3); with their result, Z^n has no lattice tiling by the Lee ball B^n(r) for any such pair. Tilings that are not lattice tilings are not covered. preprintGolombWelchRadiusThree/ holds the paper as a PDF; paper/ holds the LaTeX source (amsart) with four schematic figures; dist/ holds the PDF, the LaTeX source zip and the arXiv tarball; MasterGolombWelchRadiusThree_masterzipfinal2.zip holds every file of the repository. lean/ is a Lean 4 and Mathlib project that proves the two theorems GolombWelch.golomb_welch_35 and GolombWelch.golomb_welch_805 together with every step they rest on: the reduction of a lattice tiling to a perfect code in a finite abelian group, the ball identity in a commutative ring, the vanishing of power sums modulo a prime, the pair counts, the constant term modulo 29^2, the joint projection to Z/71 x Z/29 through dual numbers over a group ring, and two circulant systems over F_71. Both theorems depend only on the axioms propext, Classical.choice and Quot.sound. checks/ contains independent checks of the arithmetic in C, C++, Julia and Python. scripts/run_all.sh builds the Lean project, checks the axioms and runs the checks.