关于三格点一点非格点情形的四点 HRT 结果的 Lean 认证

我们记录了关于四点 Heil--Ramanathan--Topiwala 配置的 Lean 认证定理包装 $$\Lambda=\{0,a,b,\nu\}\subset \R^2, \qquad \Lzero=\Z a+\Z b, \qquad \nu=r a+s b,$$ ，其中 $a$ 和 $b$ 是线性无关的。主要认证定理表明：若 $|\symp(a,b)|>1$ 且 $1,r,s$ 相对于 $\Q$ 无线性相关，则对每一个非零 $f\in L^2(\R)$，四个向量 $$f,\qquad \pi(a)f,\qquad \pi(b)f,\qquad \pi(\nu)f$$ 必线性无关。第二个认证定理处理有理坐标情形 $r,s\in \Q$，此时配置位于更细的满秩格中，线性无关性由 Linnell 定理得出。该论文采用标准数学文体撰写。附录记录了精确的 Lean 认证账本以及形式化发展所使用的显式分析输入，并提供了下载链接。