AI Proof WatchKeep up with AI contributions

Linear dependence of time-frequency shifts of a Schwartz function

Markus Faulhuber, Philipp Petersen, Jordy Timo van Velthoven, Felix Voigtlaender

A nonzero Schwartz function has twelve distinct time-frequency shifts, eleven in one irrational translate of a half-integer lattice plus the origin, that are linearly dependent. The authors also prove a finite counterexample without a fixed twelve-shift count.

Sources for this record

What was already known

HRT predicted independence for every nonzero L² function and finite distinct shift set. Earlier results covered discrete-subgroup shifts and other special configurations.

AI involvement AI-centered

The authors credit GPT-5.6 Pro with the counterexample and retained strategy. Faulhuber, Petersen, van Velthoven and Voigtlaender directed the search, repaired the proof and supplied the Schwartz strengthening.

The final argument retains the model-origin counterexample and strategy, while humans performed essential repairs and Schwartz-class strengthening.

Importance Major

Refutes the general HRT conjecture with a Schwartz-class example.

Limitations

The human authors repaired substantial gaps in the model’s proof and strengthened its example from C³ to Schwartz class. The explicit twelve-shift step uses a reported Arb interval certificate.

Technical verification Formal (certified interval computation with python-flint/FLINT-Arb; exact rational bounds + human)

The human authors report a complete independent check and rewrite of all AI-influenced material. The twelve-shift construction additionally rests on an Arb interval certificate; this is a source-reported check, not an AIProofWatch rerun.

Formal checking

All AI-influenced parts of the twelve-shift and qualitative Schwartz counterexample proofs. independent proof verification, repair, validation, and rewrite

Checker
Markus Faulhuber, Philipp Petersen, Jordy Timo van Velthoven, and Felix Voigtlaender (authors)
Scope
All AI-influenced parts of the twelve-shift and qualitative Schwartz counterexample proofs
Basis
Reported by the linked checker

Uniform numerical inequalities needed for the explicit twelve-shift coefficient sequence. certified interval and exact rational computation

Checker
Supplementary Python script with FLINT/Arb
Scope
Uniform numerical inequalities needed for the explicit twelve-shift coefficient sequence
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Full

The authors explain the central vector-Zak, fixed-point, and eigenfunction construction and rewrote model-origin arguments; the account identifies and repairs specific gaps.

Correction and publication history