Lean-certified four-point HRT results for three lattice points and one off-lattice point
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866908988102148096 |
|---|---|
| author | Oussa, Vignon |
| author_facet | Oussa, Vignon |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_21228 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Lean-certified four-point HRT results for three lattice points and one off-lattice point Oussa, Vignon Functional Analysis 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. |
| title | Lean-certified four-point HRT results for three lattice points and one off-lattice point |
| topic | Functional Analysis |
| url | https://arxiv.org/abs/2604.21228 |