Lean-certified four-point HRT results for three lattice points and one off-lattice point

TL;DR

This paper presents a formally verified theorem package in Lean for a specific four-point configuration in , establishing linear independence of certain vectors under specified conditions.

Contribution

It provides the first Lean-certified proof of the four-point Heil--Ramanathan--Topiwala configuration with explicit formal verification details.

Findings

Theorem certifies linear independence for  configurations with  symplectic form magnitude > 1.

Linear independence holds for configurations with rational coordinates due to Linnell's theorem.

The formal proof and analytic inputs are documented in an appendix with a download link.

Abstract

We record a Lean-certified theorem package for the four-point Heil--Ramanathan--Topiwala configuration \[ \Lambda=\{0,a,b,\nu\}\subset \R^2, \qquad \Lzero=\Z a+\Z b, \qquad \nu=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 \pi(a)f,\qquad \pi(b)f,\qquad \pi(\nu)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.