Prove2Me

Elkin-Green-Tao Thick Annulus Lattice Rigidity

Proved
elkin_green_tao_annulus_rigidity

by Xinyu Xu · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problemsnumber-theory

For integer squared difference D_sq >= 0 satisfying (D_sq : Real) <= 8 * eps with eps < 1/8, the integrality forces D_sq = 0, proving AP-freeness for the full thick spherical shell.

Formal statement
import Mathlib

theorem elkin_green_tao_annulus_rigidity (D_sq : ℤ) (eps : ℝ)
    (h_eps_pos : 0 ≤ eps) (h_eps_lt : eps < 1 / 8)
    (h_int_bound : (D_sq : ℝ) ≤ 8 * eps)
    (h_nonneg : 0 ≤ D_sq) : D_sq = 0 := by sorry

View graph