Lean-certified four-point HRT results for three lattice points and one off-lattice point
Vignon Oussa
math.FA
Apr 23, 2026 · v1
TL;DR
Provides a Lean-certified theorem package proving linear independence of four-point HRT configurations with three lattice and one off-lattice point.
Abstract
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 linear independence follows from Linnell's theorem. The paper is written in standard mathematical prose. An appendix records the precise Lean certification ledger and the explicit analytic inputs used by the formal development and a download link is provided.
Problem
The Heil-Ramanathan-Topiwala (HRT) conjecture asks when finitely many time-frequency translates of a nonzero L^2 function are linearly independent. The four-point case with three lattice points and one off-lattice point remained without a machine-checked proof.
Approach
The authors produce a Lean-certified theorem package for the four-point HRT configuration {0, a, b, nu} with nu = ra + sb. The principal theorem states that if |symp(a,b)| > 1 and 1, r, s are Q-linearly independent, then f, pi(a)f, pi(b)f, pi(nu)f are linearly independent for every nonzero f in L^2(R). A second theorem treats the rational-coordinate case using Linnell's theorem.
Results
Two Lean-certified theorems are recorded: one for the irrational-coordinate case (Q-linear independence of 1, r, s) and one for the rational-coordinate case (r, s in Q). The formal development provides a complete certification ledger with explicit analytic inputs.
