{"id":"arxiv/2604.21228","url":"https://arxiv.org/abs/2604.21228","tags":["math.FA"],"score":0,"title":"Lean-certified four-point HRT results for three lattice points and one off-lattice point","domain":"math.FA","source":"arxiv","authors":["Vignon Oussa"],"reviews":0,"subject":"math.FA","summary":"We record a Lean-certified theorem package for the four-point Heil--Ramanathan--Topiwala configuration \\[ Λ=\\{0,a,b,ν\\}\\subset \\R^2, \\qquad \\Lzero=\\Z a+\\Z b, \\qquad ν=r a+s b, \\] with $a$ and $b$ linearly independent. The principal certified theorem states that if $|\\symp(a,b)|>1$ and $1,r,s$ are linearly independent over $\\Q$, then for every nonzero $f\\in L^2(\\R)$ the four vectors \\[ f,\\qquad π(a)f,\\qquad π(b)f,\\qquad π(ν)f \\] are linearly independent. A second certified theorem treats the rational-coordinate case $r,s\\in \\Q$, where the configuration lies in a finer full-rank lattice and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-04-23","reactions":{}}