The critical mixed-arithmetic four-point HRT theorem
Abstract
Although the Heil--Ramanathan--Topiwala conjecture is false in full generality, its failure makes the classification of positive geometric and arithmetic regimes more urgent. We settle the critical mixed-arithmetic regime for four time-frequency shifts. For z=(x,ω) and w=(y,η), set σ(z,w)=xη−yω. Let u,v∈R2 satisfy lvertσ(u,v)rvert=1, write ν=αu+βv, and assume that 0,u,v,ν are distinct. If dimQspanQ{1,α,β}=2 then, for every nonzero f∈ L2(R), the vectors f,π(u)f,π(v)f,π(ν)f are linearly independent. This includes both four-point configurations in Chris Heil's Conjecture~9.2. The proof first converts a putative dependence into a scalar cocycle over an irrational rotation. On a positive-measure family of zero-free fibres, winding and continued-fraction returns force the periodic holonomy to be constant. The return multiplier is Laurent polynomial, however, so its ungauged holonomy is algebraic; the constant-holonomy law simultaneously makes it an irrational character. These conclusions are incompatible. The principal theorem and its complete formal dependency chain have been fully certified end-to-end in Lean~4, including the physical all-nonzero case, the complete three-point HRT theorem, the coefficient-reduction step, and the final four-point conclusion. The accompanying \href{https://www.dropbox.com/scl/fi/jd9xeqqera147wdc82r8k/3f260460-07d5-45f5-8d1c-ee1d2879c0af-aristotle-32-.tar.gz?rlkey=a24njadfds5ty9ez473lk03lv\&e=1\&dl=0} {Lean~4 certification archive} contains reproducible source, pinned build instructions, and transitive axiom audits.
Related
- Asymptotics of holomorphic torsion on orbifolds and an equivariant arithmetic Hilbert-Samuel theorem
- Szemerédi's theorem with random differences and arithmetic Kakeya
- On a Turán's theorem for arithmetic progressions
- Fixed point properties and cohomology of Banach representations of arithmetic groups
- Performance Evaluation of an Adaptive Quadrature and a Double Exponential Formula Using Arbitrary-Precision Floating-Point Arithmetic
BibTeX
@misc{oussa2026critical,
title = {{The critical mixed-arithmetic four-point HRT theorem}},
author = {Vignon Oussa},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.27970},
eprint = {2609.27970},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.27970},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - The critical mixed-arithmetic four-point HRT theorem
AU - Vignon Oussa
PY - 2026
DA - 2026/09/01
PB - arXiv
DO - 10.48550/arxiv.2609.27970
UR - https://arxiv.org/abs/2609.27970
AB - Although the Heil--Ramanathan--Topiwala conjecture is false in full generality, its failure makes the classification of positive geometric and arithmetic regimes more urgent. We settle the critical mixed-arithmetic regime for four time-frequency shifts. For z=(x,ω) and w=(y,η), set σ(z,w)=xη−yω. Let u,v∈R^2 satisfy lvertσ(u,v)rvert=1, write ν=αu+βv, and assume that 0,u,v,ν are distinct. If dim_Qspan_Q{1,α,β}=2 then, for every nonzero f∈ L^2(R), the vectors f,π(u)f,π(v)f,π(ν)f are linearly independent. This includes both four-point configurations in Chris Heil's Conjecture~9.2. The proof first converts a putative dependence into a scalar cocycle over an irrational rotation. On a positive-measure family of zero-free fibres, winding and continued-fraction returns force the periodic holonomy to be constant. The return multiplier is Laurent polynomial, however, so its ungauged holonomy is algebraic; the constant-holonomy law simultaneously makes it an irrational character. These conclusions are incompatible. The principal theorem and its complete formal dependency chain have been fully certified end-to-end in Lean~4, including the physical all-nonzero case, the complete three-point HRT theorem, the coefficient-reduction step, and the final four-point conclusion. The accompanying \href{https://www.dropbox.com/scl/fi/jd9xeqqera147wdc82r8k/3f260460-07d5-45f5-8d1c-ee1d2879c0af-aristotle-32-.tar.gz?rlkey=a24njadfds5ty9ez473lk03lv\&e=1\&dl=0} {Lean~4 certification archive} contains reproducible source, pinned build instructions, and transitive axiom audits.
ER -