The Heil–Ramanathan–Topiwala conjecture asserts that finitely many distinct time–frequency shifts of a nonzero L^2 function are linearly independent. It was disproved with a twelve-point counterexample. The open question is whether a smaller, intrinsically subcritical counterexample exists.

The construction uses the vector-Zak and cohomological framework of Faulhuber et al., replacing their eleven-term Weyl polynomial with a three-term half-lattice polynomial composed with an irrational shift built from the cube root of 2. A dominated invariant line comes from a validated sixteen-step domination certificate computed with Arb. Multiplier winding is controlled by a two-gauge half-plane argument. An explicit Diophantine bound then yields smooth cohomological reconstruction. A Lean 4/Mathlib file corroborates the algebraic parts of the argument.

The paper exhibits four dependent time–frequency shifts of a nonzero complex-valued Schwartz function, which is minimal cardinality. Every symplectic triangle determinant of the configuration lies strictly between 0 and 1. The Lean companion compiles with Lean 4.28.0 and Mathlib with no sorry or extra axioms.