# Verification report — OWR-12339-003 (Gröchenig–Lyubarskii: is the Gaussian Gabor system over the complex lattice Λ₃ a frame?)

Verification date: 2026-10-20.

**Verdict.** The note answers the question **yes**, by a **computer-assisted proof in floating point with a margin**.
- **Settled (computer-assisted).** G(g, Λ₃) is a frame for L²(R²), g(s) = 2^{1/2}e^{−π|s|²},
  Λ₃ = A₃(Z + iZ)², A₃ = (1 2/5; 0 √21/5), with lower frame bound A_opt ≥ (10/√21)·0.23² > 0.1154 (Theorem 1.2).
  The same holds for the window e^{−π|s|²/2}, the width printed once in the source, with A_opt ≥ (5/√21)·0.18² >
  0.0353 (Theorem 1.3).
- **Nature of the proof.** The reduction to the matrix P(t, θ), the symmetries, the tail bound and the box
  inequality are proved analytically. The computational step, the inequality (5) on each of 65,597 boxes (78,318 for
  the second window), was evaluated in **IEEE double precision with an explicit rounding budget and a margin of
  10⁻⁶; it is not an interval-arithmetic computation.** The 1950 boxes with the smallest stored bound (650 for the
  second window) were re-checked in interval arithmetic with the note (`iv_check.py`), and the 2000 boxes with the
  smallest stored bound (650 for the second window) again by the third verification run with its own program and a
  different method (`independent_run_2/r2_rigorous.py`: mpmath.iv enclosures, exact positive-definiteness tests);
  all pass without the margin. Every other box has a stored bound more than 1.42·10⁻⁴ (4.8·10⁻⁵) above the target;
  these 63,597 (77,668) boxes rest on the floating-point assumption of Section 5.3.
- **Not new.** The question and the conjecture (Gröchenig–Lyubarskii, Oberwolfach Report 11/2013, p. 595; Complex
  Var. Elliptic Equ. 65 (2020), end of Sect. 4); the fiberization method (Ron–Shen 1997); matrix-valued Zak
  transform criteria for rational lattices (Zibulski–Zeevi 1997). New: the reduction of Λ₃ to the 25 × 21 matrix,
  the box inequality and the certificate.
- **Not certified / not treated.** The optimal frame bounds (A_opt = 0.12265 is numerical only); the range
  √21/5 < t < √24/5 of the source.

The note is unrefereed.

## Statement checked
- **Primary source.** K. Gröchenig (joint work with Yu. Lyubarskii), "Gabor frames and complex analysis",
  Oberwolfach Report 11/2013, *Structured Function Systems and Applications*, Oberwolfach Reports 10 (2013), no. 1,
  pp. 579–655, doi:10.4171/OWR/2013/11; the abstract pp. 593–596, read in full in the open publisher file.
  - Definitions: π(x, ξ)g(t) = e^{2πiξ·t}g(t − x); frame inequality; complex lattices Λ = A(Z + iZ)^d with
    z = x + iξ (pp. 593, 595).
  - The window is printed once as 2^{d/4}e^{−πt·t/2} (p. 594); the normalising factor, the Bargmann transform and the
    Fock weight on the same page, and the published paper (φ(x) = exp(−π|x|²)) all fit e^{−π|t|²}. The note reads the
    window as e^{−π|s|²} and covers the other reading separately (Theorem 1.3).
  - p. 595: the theorem (i) γ₁, γ₂ < 1 ⇒ frame, (ii) γ₂ ≥ 1 ⇒ not a frame (from Gröchenig, ACHA 31 (2011)); the
    matrices A₁, A₂, A₃; Λ₁ and Λ₂ do not give frames; for Λ₃ the authors conjecture a frame and have no reliable
    proof.
- **Published follow-up.** Gröchenig–Lyubarskii, Complex Var. Elliptic Equ. 65 (2020), no. 10, 1717–1735,
  doi:10.1080/17476933.2019.1681415, read in full in the arXiv version 1905.09927v1 (journal version not compared):
  Prop. 2.2, Thm 4.1, Cor. 4.2, Cor. 4.3 (Λ₁, Λ₂), the family A_t = (1 2/5; 0 t) with "do not know" for
  √21/5 ≤ t < √24/5 (end of Sect. 4), Thm 5.3 (weak reconstruction for max γ_j = 1), and the class |β|² + γ² = 1
  (end of Sect. 5), to which Λ₃ belongs.
- **Corpus record.** ulamai/UnsolvedMath, OWR-12339-003 (snapshot d371ee9; status `open`; statement
  `corrected_verified`): normalised Gaussian on R², A₃ = (1 2/5; 0 √21/5), Λ₃ = A₃(Z + iZ)², "Is G(g, Λ₃) a frame for
  L²(R²)?" This is Problem 1.1 of the note.

## Readings
| Reading | Answer | Where |
|---|---|---|
| Window e^{−π|s|²} (normalised 2^{1/2}e^{−π|s|²}), the reading supported by the source | frame, A_opt ≥ 0.1154 (computer-assisted, floating point with margin) | Theorem 1.2 |
| Window e^{−π|s|²/2} (the exponent printed once in the report) | frame, A_opt ≥ 0.0353 for the unit vector e^{−π|s|²/2} (same qualification) | Theorem 1.3 |
| Identification of (x, ξ) with x + iξ or with ξ + ix | the same lattice A₃Z² × A₃Z² (A₃ real) | Section 1.1 |
| Constant factor of the window | irrelevant for the frame property; the bounds are given for unit vectors | Lemma 2.1 |
| The range √21/5 < t < √24/5 | not treated | Section 6 |

## Results in the paper
- **Lemma 2.1 (dilation).** U f(s) = |det A₃|^{1/2} f(A₃s) turns G(g_a, Λ₃) into G(c_a φ_a, Z² × MZ²),
  M = A₃ᵀA₃ = (1 2/5; 2/5 1), φ_a(y) = exp(−πa yᵀMy), c_a² = 2a det A₃.
- **Proposition 2.2 (fiberization),** Lemma 2.3 (Γ = M⁻¹Z² ⊃ 5Z² with index 21), **Proposition 2.4 (Bloch
  reduction)** and **Corollary 2.5 (criterion):** σ_min(P_a(t, θ)) ≥ s on R⁴ ⇒ frame with A_opt ≥ (10a/√21)s², with
  P_a the explicit 25 × 21 matrix (3) of Gaussian lattice sums. Only this implication is used (Remark 2.6: converse,
  not used).
- **Lemmas 3.1, 3.2.** Symmetries (θ-periodicity, translations by Z² + Γ = Zw₁ + Zw₂, t ↦ −t, θ ↦ −θ) reduce R⁴ to
  the box D = [0,1] × [0,1/2] × [0,1/2] × [0,1]; gauge and 9-term window (4).
- **Lemma 4.1 (tail)** for every a: τ₁ < 2.1·10⁻⁴², ‖T‖₂ < 4.8·10⁻⁴¹; τ_{1/2} < 6.0·10⁻²¹, ‖T‖₂ < 1.4·10⁻¹⁹.
  **Proposition 4.2 (box inequality):** σ_min ≥ σ_min(Pw(z⁰)) − E₁ − R₂ − √525 τ_a on a box (vertex bound for the
  first-order term, entrywise second-order Taylor remainder).
- **Section 5.** The certificate (65,597 / 78,318 boxes; smallest computed bound 0.2300001490 / 0.1800000626), its
  checks, the floating-point assumption and its estimate, measured errors, the interval re-check, and the proofs of
  Theorems 1.2 and 1.3.

## Computations (programs and outputs in reproducibility/)
- **Program written with the note** (`check_note.py`, standard library, about 15 s; TOTAL failures: 0): exact
  lattice arithmetic (M, det M, 10/√21, Γ ∩ Z² = 5Z², index 21, residue systems in both certificates, Z² + Γ =
  Zw₁ + Zw₂, the covering of R⁴ by D on 20,000 exact random points); the tail bounds; the lattice facts of Section 6;
  a pure-Python symbol (σ_min = 0.2370731445 at the numerical minimiser; P*P = Gram symbol of the k-sums at a random
  point, 7.8e-16; the exact zero for Λ₁, λ_min = 4e-17; the symmetries, 2.8e-16); the certificates read without
  NumPy: exact cover of the finest dyadic grid (16,777,216 cells) by the 65,597 and by the 78,318 boxes, and the box
  test recomputed for 60 boxes of each (largest deviation from the stored values 6.1e-16); the constants of the
  theorems.
- **Interval re-check written with the note** (`interval_check/iv_check.py`, mpmath.iv, 30 digits, from exact
  rational data): 1950 boxes (a = 1) and 650 boxes (a = 1/2) with the smallest stored bound; interval Cholesky
  factorisations prove ‖X_ε‖₂ < μ and σ_min(Pw(z⁰)) > s + μ + R₂ + τ; all pass, without the 10⁻⁶ margin (smallest
  float difference σ̂_min − s_req: 1.149e-6 for a = 1). About 2.1 s per box.
- **Programs with which the result was first obtained** (`original/`): `certify.py` (93 s / 111 s), the standalone
  checker `check_certificate.py` (partition, residue systems, every box; deviation from stored 7.8e-16 / 6.9e-16;
  Gram cross-check at 1500 centres 2.9e-15), `rejection_tests.py` (8 corruptions rejected), `hp_check.py` (σ_min and
  E₁, not R₂, at 30 digits for 300 boxes: 2.2e-16, 2.1e-17), `indep_gram.py` (9.4e-16), `reduction_check.py`
  (frame sums in the original coordinates against the fibre formula: ≤ 1.4e-15), `invariance_check.py` (1.7e-15),
  `explore_min.py` (numerical minimum 0.2370731445 at t = (1/14, 1/14), θ = (1/2, 1/2)), `known_cases.py`,
  `lambda1_test.py` (Λ₁: σ_min = 2.6e-16; (4/5)I: 0.4545).

## Independent verification runs
The result was first obtained with the programs in `original/`. Two independent verification runs, both
AI-assisted, followed (2026-10-20), each with its own programs. The interval re-check and `check_note.py` were
written afterwards, with the note; these two runs did not examine them. A third independent verification run,
also AI-assisted, then examined the text of the note and this package (section below).

| Item | Run A | Run B |
|---|---|---|
| Statement, window convention, lattice identification against the source | CONFIRMED (OWR pp. 593–595, CVEE Sect. 1, 2, 4) | CONFIRMED (OWR p. 594–595, CVEE p. 2 and Sect. 4) |
| Dilation, fiberization, Bloch reduction, constant 10/√21 | CONFIRMED (re-derived; end-to-end identity tests: closed form 1.486870073881227 reproduced by the fibre and the Bloch side to 3e-15) | CONFIRMED (re-derived; independent route: duality + rational noncommutative 4-torus, 21 × 21 symbol, A_opt = 0.1226464757, agreement 1e-10) |
| Symmetries and the box D | CONFIRMED (re-derived) | CONFIRMED (re-derived, both reflections) |
| Box inequality (vertex bound, Taylor remainder, envelopes, tail) | CONFIRMED (re-derived); tail for a = 1/2 to be stated (fix) | CONFIRMED (code review of the checker); tail for a = 1/2 to be stated (fix) |
| Certificate | CONFIRMED by own checker on all boxes (partition by occupancy counting; deviation 7.8e-16); 30 tightest boxes at 30 digits incl. R₂ | CONFIRMED (re-run of certify.py byte-identical; checker PASS); own certificate in its own formulation: A_opt ≥ 0.1220 (a = 1), ≥ 0.0393 (a = 1/2), double precision, margin 1e-8 |
| Known cases | CONFIRMED (Λ₁ zero, (4/5)I positive, own code) | CONFIRMED (Λ₁, Λ₂ zero; theorem (i)/(ii) controls) |
| Literature / novelty | consistent (arXiv API, Crossref, 1 web search) | consistent (Semantic Scholar citations 9 + 38, closest works read beyond the abstract, 1 web search) |
| Floating point | proof rigorous modulo the floating-point assumption; not interval-verified | not interval-verified |

Required fixes (all made; listed in the paragraph "Verification" of the note): tail bound for a = 1/2 (Lemma 4.1);
bibliographic data of Gjertsen–Luef and of the CVEE paper from Crossref; say that `hp_check.py` does not recompute R₂
and cite the 30-digit R₂ recomputation of run A (Section 5.3); keep the floating-point qualification next to the
result; only the implication σ_min ≥ s ⇒ frame is used (Corollary 2.5).

## Third independent verification run (on the text of the note), 2026-10-20
AI-assisted; its own programs and outputs are in `reproducibility/independent_run_2/` (they share no code with
the package or the earlier runs).

| Item | Result |
|---|---|
| Statement against the source (OWR pp. 593–596, read again in full; CVEE arXiv v1, Prop. 2.2, Thm 4.1, Cor. 4.2, 4.3, end of Sect. 4 and 5, Thm 5.3) | CONFIRMED; Problem 1.1 is the question as posed and the record's question; window reading correct, other reading covered |
| Sections 2–4 (dilation, fiberization, lattice data, Bloch reduction, criterion, Remark 2.6, symmetries, domain, gauge, tail, box inequality) | CONFIRMED (re-derived line by line; no gap) |
| Reduction end to end | CONFIRMED: frame sums of random generalised Gaussians in the original coordinates (closed-form inner products) against the Bloch side, a = 1 and 1/2: relative difference ≤ 3.5e-15; P*P = Gram symbol of Remark 2.6 to 1.9e-15 |
| Box test in double precision, every box | CONFIRMED by own code: 0/65,597 and 0/78,318 below target, deviations from stored ≤ 5.6e-16 / 6.4e-16; exact cover of D (occupancy of 16,777,216 cells and exact total volume); residue systems exact |
| Rigorous re-check | the 2000 (a = 1) and 650 (a = 1/2) boxes with the smallest stored bound: 2000/2000 and 650/650 PASS without the margin (own upper bounds for E₁, R₂, tail from mpmath.iv enclosures; positive definiteness decided exactly by Sylvester's criterion in integer arithmetic); smallest slack 1.149e-6 / 1.063e-6; target raised by 2e-6: the 3 tightest boxes FAIL (control) |
| Tail bounds | recomputed in interval arithmetic: τ₁ ≤ 2.0716e-42, √525τ₁ ≤ 4.7466e-41, τ_{1/2} ≤ 5.7572e-21, √525τ_{1/2} ≤ 1.3192e-19 |
| Numbers of Remark 1.4 and Sect. 5.3, 6 | σ_min = 0.2370731445 at t = (1/14, 1/14), θ = (1/2, 1/2); A_opt = 0.1226464757; a = 1/2: 0.19399, A_opt 0.04106; B ≈ 2.334; ranges π yᵀM_a y ≤ 509.1, \|2πν·θ\| ≤ 14.1, derivative factors ≤ 19.1; Λ₁ zero (6.7e-16) |
| Package re-run from the archive | certify.py byte-identical (both certificates); check_certificate, rejection tests, indep_gram, reduction, invariance, known cases, Λ₁, explore_min, hp_check (300 boxes), run A's programs: outputs identical; iv_check (first 60 + 30 boxes) identical lines; check_note.py TOTAL failures 0 |
| Literature | arXiv API, zbMATH Open, Crossref (and all 20 DOIs), OpenAlex (7 works citing CVEE 2020, 2 citing the OWR report), one web search: no printed answer; one further citing work (two-dimensional Gaussian lattice sums) added to the list of abstracts read |
| Verdict | CONFIRMED as a computer-assisted proof with the stated floating-point qualification; no mathematical error; not fatal |

Required fixes of this run (all made): record this run in the note (paragraph "Verification", Section 5.3, list of
folders in Section 7) and here; state the rigorous coverage (2000 / 650 boxes) in the abstract, Theorem 1.2, Section
5.3 and "Scope and priority"; add its searches and the further citing work to "Scope and priority".

## Relation to the literature, novelty and scope
- **Searches (19–20 October 2026).** arXiv API (Gaussian Gabor frames and lattices; Bargmann–Fock lattices; complex
  lattices; computer-assisted Gabor frames; multivariate Gaussian Gabor systems; sorted by date), zbMATH Open
  (Gabor and Gaussian in the title, 2014–2026), Crossref, the citation lists of the CVEE paper (Semantic Scholar 9,
  OpenAlex 7) and of Gröchenig's ACHA paper (OpenAlex 23, Semantic Scholar 38), and three web searches for the
  specific lattice; the third verification run repeated queries to the arXiv API, zbMATH Open, Crossref and
  OpenAlex (works citing the CVEE paper and the OWR report) and made one further web search. No printed answer was found; none of the works found treats Λ₃ or the range
  √21/5 ≤ t < √24/5.
- **What was read.** The source abstract in full; the CVEE paper in full (arXiv v1). Of Luef–Wang (GAFA 2023), the
  main statements and Sections 4.1–4.2; of de Dios Pont–Liehr–Taylor (2026), Theorem 1.2; of Ulanovskii–Zlotnikov
  (2026), the full text (one-dimensional); of Luef–Testorf–Wang, Romero–Ulanovskii–Zlotnikov, Gjertsen–Luef and
  Pfander–Rashkov, the statements of the main results; of Liu–Ma–Zheng, Enstad–Thiel–Vilalta and five further
  citing works on other subjects (among them Bétermin–Faulhuber–Steinerberger on two-dimensional Gaussian lattice
  sums), the abstracts. Gröchenig (ACHA 2011), Lyubarskii (1992), Seip (1992),
  Seip–Wallstén (1992) are quoted as stated in the source and in the CVEE paper. Ron–Shen, Zibulski–Zeevi and
  Gröchenig's book are cited for the method; the identities used are proved in the note. All bibliographic data
  were checked with Crossref and the arXiv API.
- **Consistency.** Neither part of Prop. 2.2 of the CVEE paper applies to any basis of Λ₃ (its lattice minimum is
  1); Λ₃ is not in the non-frame families of CVEE Thm 4.1, Cor. 4.2, 4.3; CVEE Thm 5.3 applies but gives only a weak
  reconstruction formula; the covolume criterion of Luef–Wang needs vol < 1/2; the criterion of de Dios
  Pont–Liehr–Taylor, Thm 1.2, concerns lattices of integer density (Λ₃ has density 25/21).
- **Scope.** A search that finds nothing is not a proof of novelty; no priority is claimed beyond the reduction, the
  box inequality and the certificate. The certificate is in floating point with a margin, not interval-verified
  except for the 2000 (650) boxes listed above.

## Public release and license
This paper, its source files, and this verification report are licensed under the Creative Commons Attribution
4.0 International License (CC BY 4.0): https://creativecommons.org/licenses/by/4.0/