The Gaussian Gabor System over the Complex Lattice Λ₃ of Gröchenig and Lyubarskii Is a Frame: A Computer-Assisted Proof

Gröchenig and Lyubarskii (Oberwolfach Report 11/2013) considered the Gabor system G(g, Λ₃) of time-frequency shifts of the Gaussian g(s) = 21/2 e−π|s|² on R² along the complex lattice Λ₃ = A₃(Z + iZ)², A₃ = (1 2/5; 0 √21/5). They conjectured that it is a frame for L²(R²) and wrote that they had no reliable proof; in their paper in Complex Var. Elliptic Equ. 65 (2020), Λ₃ is the end point t = √21/5 of a range √21/5 ≤ t < √24/5 of lattices for which the answer is stated to be unknown. We prove the conjecture by a computer-assisted proof in floating point with a margin. A dilation turns G(g, Λ₃) into a Gabor system over the rational separable lattice Z² × MZ², M = (1 2/5; 2/5 1). The fiberization of Ron and Shen and a Bloch reduction over 5Z² show that the system is a frame with lower bound (10/√21)s² as soon as an explicit 25 × 21 matrix P(t, θ) of Gaussian lattice sums satisfies σ_min(P(t, θ)) ≥ s > 0 for all (t, θ) ∈ R⁴. After a reduction by symmetries to a box in R⁴, a branch-and-bound computation over 65,597 boxes, with a first-order bound maximised over the vertices of each box, a rigorous bound for the second-order Taylor remainder and an explicit tail bound, gives σ_min(P) ≥ 0.23 everywhere. Hence G(g, Λ₃) is a frame with lower frame bound at least 0.1154 (numerically the optimal bound is 0.12265). The box inequalities were evaluated in IEEE double precision with an explicit rounding budget and a margin of 10⁻⁶, not in interval arithmetic; two independent recomputations in interval arithmetic, of the 1950 and of the 2000 boxes with the smallest margin, confirm these boxes without the margin. The same conclusion holds for the window e−π|s|²/2, the width printed once in the report (σ_min ≥ 0.18). The question and the conjecture are due to Gröchenig and Lyubarskii; no printed answer was found in the sources searched. This is an unrefereed note. Unrefereed preprint released for independent mathematical scrutiny. Publication on Zenodo does not constitute peer review. AI-assisted tools supported research, computation, proof development, and manuscript preparation. The author remains responsible for all claims and the final text. Corpus identifier: OWR-12339-003 (Gröchenig–Lyubarskii, Gabor frames and complex analysis, Oberwolfach Report 11/2013, p. 595).