An intrinsically subcritical four-point counterexample

Vignon Oussa

REVIEW 1 major objections 6 minor 19 references

An intrinsically subcritical four-point counterexample

T0 review · 1 major / 6 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper presents a computer-assisted proof that the HRT conjecture fails for four time–frequency shifts of a nonzero Schwartz function, with every symplectic triangle determinant strictly between zero and one.

desk verdict A genuine four-point subcritical counterexample to HRT that is analytically coherent but rests on unexecutable validated-numerics certificates, deserving a serious referee who can actually run the accompanying Arb code. read the letter →

arxiv 2608.07604 v1 pith:NXP35K5S submitted 2026-08-06 math.CA math.DS

Vignon Oussa This is my paper · ORCID

classification math.CAmath.DS MSC 42C1537D3065G30

keywords HRTconjecturetime-frequencyshiftsWeyloperatorsvectorZaktransformdominatedcocyclevalidatednumericsSchwartzfunctionssubcriticalconfiguration

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper disproves the HRT conjecture at the smallest possible cardinality: it exhibits an explicit nonzero Schwartz function whose four time-frequency shifts are linearly dependent. The four phase-space points are built from cube roots of two, and every symplectic triangle they determine has absolute value strictly below one, so the configuration is intrinsically subcritical. The proof passes through a two-component vector Zak transform, turning the problem into a matrix cocycle over an irrational torus translation, then uses computer-assisted interval-arithmetic certificates to construct a smooth invariant line and to solve the corresponding cohomological equation. If the proof is correct, the known counterexample size drops from twelve points to four, and the irrational subcritical regime is the home of such dependent configurations.

What carries the argument

The central object is the two-component vector Zak transform, a unitary map that presents functions on the line as sections of a two-dimensional vector bundle over the torus and converts Weyl shifts into a matrix-valued cocycle $B(x,\omega)=\eta(x)A(x,\omega)$ with $A=I+\tfrac{3}{5}e^{-\pi i\omega}D+\tfrac{3}{5}e^{\pi i x}S$, where $D$ and $S$ are the diagonal and permutation matrices, over the irrational translation $T(x,\omega)=(x-\alpha,\omega-\beta)$. The load-bearing mechanism is a smooth dominated splitting of the iterated cocycle $B^{16}$, obtained from four validated interval-arithmetic certificates that control singular-value ratios, junction overlaps, and a rotated half-plane gauge; this yields a smooth invariant line. On that line the multiplier equation reduces to a cohomological equation $q_{\mathrm{sm}}(z)h(Tz)=\lambda h(z)$, solved with an explicit Diophantine bound coming from the algebraic norm in $\mathbb{Q}(\sqrt[3]{2})$. The resulting smooth vector-Zak section pulls back to the Schwartz eigenfunction $g$.

What would settle it

Recompute the four certificate inequalities on a finer grid (at least $1024^2$ per fundamental rectangle) with a different interval-arithmetic implementation and compare against the paper's printed global lower bounds: gap above $3.5398$, junction above $15\,399\,575.8$, overlap lower bound above $48.8768$, and half-plane lower bounds above $74.9429$; a single violation would collapse the domination, the invariant line, and the eigenfunction construction.

Watch

Extended reading notes

Core claim

The paper's main theorem asserts that there exist a nonzero complex-valued Schwartz function $g$ and a nonzero constant $\lambda$ such that $\left[ I + \tfrac{3}{5}\rho(1,0) + \tfrac{3}{5}\rho(0,1/2) \right] \rho(\zeta) g = \lambda g$, with $\zeta = (\alpha,\beta/2)$, $\alpha=\sqrt[3]{2}-1$, and $\beta=\sqrt[3]{4}-1$. Equivalently, the four shifted copies displayed in (1.5) are linearly dependent. The four points are distinct, no three are collinear, and every absolute symplectic triangle determinant lies strictly between zero and one, so every admissible re-marking of the configuration is subcritical. The construction is computer-assisted: validated interval-arithmetic certificates establish a dominated splitting and a half-plane gauge, and exact cohomological arguments complete the eigenfunction.

Load-bearing premise

The proof's four computer-assisted interval-arithmetic checks are the load-bearing premise: if any of their inequalities is violated, the dominated splitting, the invariant line, and the Schwartz eigenfunction can fail, and the paper's formal companion explicitly does not cover this computational core.

Editorial extensions

If this is right

One-, two-, and three-point systems are always linearly independent, so four is the minimal possible size of a counterexample to the HRT conjecture.
This is the first counterexample in the intrinsically subcritical regime: all four absolute symplectic triangle determinants are below one, and the background lattice covolume is $1/2$.
The maximally irrational subcritical cell of the four-point dashboard is nonempty, so the open classification of dependent four-point configurations now has a concrete member in that cell.
The four certificate inequalities are the only computer-assisted premises; the paper's formal companion verifies exact algebraic steps but deliberately does not formalize the interval-arithmetic computation.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Varying the two coefficients $3/5$ or replacing $\sqrt[3]{2}$ by another cubic irrationality may yield further four-point counterexamples, provided the corresponding domination and overlap certificates still pass; this is a testable extension, not a paper claim.
The explicit Diophantine bound (7.1) is strong enough that the cohomological step should work for any pair $\alpha,\beta$ of the same algebraic shape, so the construction is not tied to the particular numerical values.
Because all four triangle areas are below one while dependence still occurs, area and covolume thresholds alone do not prevent dependence; the arithmetic of the rogue point's coordinates may be the controlling ingredient.
An independent, differently implemented re-run of the four certificates would either confirm the proof or locate the point where the domination, overlap, or gauge argument breaks; the paper itself flags the computational core as the unformalized part.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Kevin — here's my read on Oussa's four-point HRT counterexample.

The paper is a genuine strengthening of the Faulhuber–Petersen–van Velthoven–Voigtlaender result. It reduces the dependent configuration from twelve points to four, and it does so in the intrinsically subcritical regime — every triangle determinant is strictly below one, and no re-marking leaves that row of the dashboard. That is new and substantial. The analytic architecture is coherent: exact Zak reduction, the three-term Weyl symbol, the 16/32-block domination certificates, the two-gauge winding argument, and the cubic Diophantine estimate all fit together. The paper is also unusually honest about provenance; Section 9 names what is adapted and what is new, and the Lean file is described at exactly the right level of overstatement — algebraic corroboration, not end-to-end formalization.

The soft spot is the one you flagged. Theorem 4.2 is the sole computer-assisted input, and the four certificate inequalities carry the construction. The manuscript describes the finite-cover method, the cell allowances, and the concrete margins, but the actual Python/Arb programs are only in a Dropbox supplement, not in the preprint, and the 1024^2 cross-check shares low-level routines with the primary code. So the correctness of the main theorem, as it stands in the arXiv file, depends on computations the reader cannot run or inspect from the text. That is a real limitation, but it is the standard limitation of validated-numerics proofs. The description is detailed enough to make the claims plausible, and the margins are large (the junction margin is ~1.5e7), so this is not a case where a tiny numerical error is likely to flip the result.

My bottom line: the paper deserves a serious referee, not a desk rejection. The referee should be asked to obtain the supplement, run the Arb programs, and check that the printed bounds match. The authors should also be encouraged to package the code in a way that survives peer review — a GitHub repository or a journal-hosted appendix would be better than a Dropbox link. If the supplement reproduces the stated bounds, the proof is convincing.

For the reading group: worth a session, but with a laptop ready to poke at the code. I would cite it if I worked in this area.

Referee Report

1 major / 6 minor

Summary. The paper presents a computer-assisted construction of four time-frequency shifts of a nonzero Schwartz function that are linearly dependent, contradicting the HRT conjecture in the four-point, intrinsically subcritical regime. The proof uses the two-component vector Zak transform to reduce the problem to a cocycle over the irrational torus translation z ↦ z − (α, β), with α = ∛2 − 1 and β = ∛4 − 1. Under four numerical certificates (C1)–(C4) stated in Theorem 4.2, the author constructs a dominated invariant line for the sixteen-step cocycle, proves zero winding of the associated multiplier by a rotated-half-plane gauge argument, solves a cohomological equation using an explicit Diophantine bound, and reconstructs the Schwartz eigenfunction. The paper also proves that all four symplectic triangle determinants of the configuration lie strictly between zero and one, so the configuration is intrinsically subcritical.

Significance. If the computational certificates are correct, the result is a substantial advance in the HRT problem: it reduces the known counterexample from twelve points to four and places the counterexample in the previously open subcritical regime. The analytic architecture is largely transparent and exact: the geometry in Section 2, the linear-algebra reductions in Lemma 4.1, the cone estimates in Section 5, and the Diophantine bound in Lemma 7.1 are all presented with explicit constants. The paper is also admirably honest about the scope of its formal verification: Section 10 states that the Lean companion does not formalize Arb or the computational certificates, so the certificates themselves remain the load-bearing input. The main weakness is that this input is not auditable from the manuscript as submitted, because the certificate code and exact logs are not included and no URL is provided.

major comments (1)

[§5, Lemma 5.2 and Proposition 5.3; §6, Lemma 6.1] The four certificates (C1)–(C4) are the sole computer-assisted input to the proof, and every later step—the dominated splitting in Section 5, the gauge overlap in Section 6, the winding transfer, and Theorem 1.1—depends on them. The 'Validated verification' paragraph reports only summary numbers (e.g., global lower bounds 3.5398, 15,399,575.8, 48.876, and 74.94) and the actual Python/Arb programs are not included or linked in the manuscript. Section 10 explicitly says the Lean companion does not formalize Arb or the computational certificates. As submitted, the main theorem cannot be checked from the paper alone, because a single error in coefficient expansion, cell derivative allowance, or cover logic would invalidate the invariant-line construction. I request that the complete certificate code, exact output logs, and the precise rational ball endpoints be made available as ancillary files, and that the relationship between the printed decimal bounds and the exact statements in Theorem 4.2 be spelled out.

minor comments (6)

[§4, after Theorem 4.2] The sentence 'By Theorems 4.1 and 4.2' should read 'By Lemma 4.1 and Theorem 4.2'; there is no Theorem 4.1.
[§5, Proposition 5.3] The references to 'Theorem 5.1' and 'Theorem 5.2' should be to Lemma 5.1 and Lemma 5.2.
[§4, 'Validated verification'] The description of the 1024² implementation as 'independently formulated' is misleading, since the next sentence discloses that it shares the low-level Laurent-product and Hermitian-polynomial routines; I suggest using 'separately formulated' and making clear that it is not an independent software-stack check.
[§10] The supplement is said to be available on Dropbox, but no URL or manifest content is included in the manuscript; for a computer-assisted proof, the code and logs should be bundled as ancillary files with the submission.
[§5, Lemma 5.2] The regularity proof of the invariant section is highly compressed; since smoothness of the section is used in the Fourier-cohomology step in Section 7, please provide a precise reference to [9] with a chapter or theorem number, or expand the jet-contraction argument.
[§2, Proposition 2.1] The inference '1 + α + β < 2' does not follow from the stated inequalities 0 < α < 1 and 0 < β < 1 alone; the stronger bounds α < 1/3 and β < 2/3 should be stated explicitly.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: Theorem 1.1 is an explicit computer-assisted construction whose certificates and analytic chain are not defined in terms of the conclusion; the unverified computational core is a transparency risk, not a circular step.

full rationale

The claimed derivation is not equivalent to its inputs. The main theorem asserts existence of g and lambda for the explicit operator I + (3/5)rho(1,0) + (3/5)rho(0,1/2) acting on rho(zeta). The proof constructs F = h v_sm as a solution of B(z)F(Tz)=lambda F(z); the existence of v_sm, h, and lambda follows from the validated certificates (C1)-(C4) plus standard contraction and cohomology arguments, not from assuming the conclusion. The constants alpha, beta, zeta, and 3/5 are design choices of the construction, and the geometric claims are proven exactly in Proposition 2.1. Prior work [5] supplies methodology (vector-Zak transform, sewing, graph transform) but the present paper re-proves the needed vector-Zak identities in Section 3 and the graph-transform lemmas in Section 5, so there is no imported uniqueness theorem that forces the result. The self-citations [14]-[16] appear in the dashboard, which Section 1 explicitly states is included only to locate the result and is not used as an input to the proof. The only caveat of substance is non-circular: Theorem 4.2's certificates (C1)-(C4) are the sole computational input, the programs are not contained in the preprint, and Section 10 states the Lean artifact is an algebraic corroboration that does not formalize Arb's implementation, the vector Zak transform, graph-transform regularity, winding classes, Fourier cohomology, or Schwartz reconstruction; the 1024^2 cross-check is itself described as not an independent software-stack replication or an additional premise. These are verification and transparency limitations to be weighed separately; they do not make the derivation circular.

Assumptions & free parameters 4 free parameters · 5 assumptions · 0 invented entities

The proof is self-contained modulo standard theorems and the computer certificates. The hand-chosen constants alpha, beta, 3/5, and the gauge rotation are part of the explicit construction, not fitted to external data. The dominant unverified premise is the reliability of the custom Arb/FLINT validated-numerics routines.

free parameters (4)

alpha (cuberoot(2)-1) = approximately 0.2599210499
Defines the phase-space shift zeta=(alpha,beta/2). Chosen by hand so the background covolume is 1/2 and all four triangle determinants lie in (0,1). Exact algebraic number, not fitted to data.
beta (cuberoot(4)-1) = approximately 0.5874010517
Companion arithmetic parameter; with alpha it produces the irrational torus translation tau=(alpha,beta). Chosen by hand for the subcritical geometry and the Diophantine estimates.
coefficient 3/5 in three-term symbol = 3/5
The weights in the operator I+(3/5)rho(1,0)+(3/5)rho(0,1/2) are hand-selected so that the validated domination and overlap certificates pass. Load-bearing for the computer-assisted part.
rotation angle -3*pi/7 in (C4) and Lemma 6.1 = e^{-3*pi*i/7}
Ad hoc gauge rotation used to put the reference multiplier q_ref in a right half-plane and conclude zero winding. Chosen so that the linear gauge certificate returns a positive real part; a proof device, not a physical parameter.

assumptions (5)

standard math Smooth-Zak characterization: a C-infinity quasi-periodic vector-Zak section with the sewing laws (3.3)-(3.4) is the Zak transform of a Schwartz function.
Invoked in Section 8 to promote the reconstructed L^2 eigenfunction to S(R). Standard external theorem from Grochenig, Theorem 8.2.5.
standard math Uniqueness theorem for dominated splittings of prescribed fiber dimension.
Used in Lemma 5.4 to prove that the constructed splitting is unique and hence one-step invariant. Relies on the standard statement by Bochi-Gourmelon.
domain assumption Correctness of Arb/FLINT interval arithmetic and the custom Python certificate programs.
Theorem 4.2's four inequalities are delegated to validated-numerics programs. The text summarizes bounds but does not include a machine-checkable proof of the programs, and the Lean artifact explicitly excludes the Arb core.
standard math Exponential lifting criterion and standard Fourier cohomology on the torus.
Used in Propositions 6.2 and 7.2 to pass from zero winding to a smooth logarithm and to solve the multiplicative coboundary equation via small-divisor bounds.
standard math Algebraic irreducibility of X^3-2.
Used in Proposition 2.2 to establish rational independence of 1, alpha, beta. Standard algebra.

how reviews work

0 comments

Cite this review

Pith. "Pith review of An intrinsically subcritical four-point counterexample." pith.science (2026). https://pith.science/paper/NXP35K5S

@misc{pith2026260807604,
  author       = {Pith},
  title        = {Pith review of: An intrinsically subcritical four-point counterexample},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/NXP35K5S}},
  note         = {Machine review of arXiv:2608.07604}
}

read the original abstract

Building on the vector-Zak and cohomological framework developed by Faulhuber, Petersen, van Velthoven, and Voigtlaender in their twelve-point counterexample, we give a computer-assisted four-point counterexample with a nonzero complex-valued Schwartz window. Every symplectic triangle determinant of the explicit configuration has absolute value below one, placing it in the intrinsically subcritical regime.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages

[1]

Jairo Bochi and Nicolas Gourmelon,Some characterizations of domination, Math. Z. 263(2009), no. 1, 221–231

work page 2009
[2]

12699, Springer, 2021, pp

Leonardo de Moura and Sebastian Ullrich,The Lean 4 theorem prover and programming language, Automated Deduction—CADE 28, Lecture Notes in Computer Science, vol. 12699, Springer, 2021, pp. 625–635

work page 2021
[3]

Ciprian Demeter,Linear independence of time frequency translates for special configu- rations, Math. Res. Lett.17(2010), no. 4, 761–779

work page 2010
[4]

Ciprian Demeter and Alexandru Zaharescu,Proof of the HRT conjecture for(2, 2) configurations, J. Math. Anal. Appl.388(2012), no. 1, 151–159

work page 2012
[5]

Linear dependence of time-frequency shifts of a Schwartz function

Markus Faulhuber, Philipp Petersen, Jordy Timo van Velthoven, and Felix Voigt- laender,Linear dependence of time–frequency shifts of a Schwartz function, 2026, arXiv:2608.05044v1; ancillary Arb code. AN INTRINSICALLY SUBCRITICAL FOUR-POINT COUNTEREXAMPLE 19

work page Pith review arXiv 2026
[6]

Karlheinz Gröchenig,Foundations of time-frequency analysis, Applied and Numerical Harmonic Analysis, Birkhäuser, Boston, MA, 2001

work page 2001
[7]

Christopher Heil,Linear independence of finite Gabor systems, Harmonic Analysis and Applications, Birkhäuser, Basel, 2006, pp. 171–206

work page 2006
[8]

Christopher Heil, Jayakumar Ramanathan, and Pankaj Topiwala,Linear independence of time-frequency translates, Proc. Amer. Math. Soc.124(1996), no. 9, 2787–2795

work page 1996

Show all 19 references

[9]

Hirsch, Charles C

Morris W. Hirsch, Charles C. Pugh, and Michael Shub,Invariant manifolds, Lecture Notes in Mathematics, vol. 583, Springer, Berlin, 1977

1977
[10]

Comput.66(2017), no

Fredrik Johansson,Arb: Efficient arbitrary-precision midpoint-radius interval arith- metic, IEEE Trans. Comput.66(2017), no. 8, 1281–1292

2017
[11]

Linnell,Von Neumann algebras and linear independence of translates, Proc

Peter A. Linnell,Von Neumann algebras and linear independence of translates, Proc. Amer. Math. Soc.127(1999), no. 11, 3269–3277

1999
[12]

Fourier Anal

Wencai Liu,Letter to the editor: Proof of the HRT conjecture for almost every(1, 3) configuration, J. Fourier Anal. Appl.25(2019), no. 4, 1350–1360

2019
[13]

Moore, R

Ramon E. Moore, R. Baker Kearfott, and Michael J. Cloud,Introduction to interval analysis, Society for Industrial and Applied Mathematics, Philadelphia, PA, 2009

2009
[14]

Okoudjou and Vignon Oussa,Letter to the editor: On a special configuration for the HRT conjecture, J

Kasso A. Okoudjou and Vignon Oussa,Letter to the editor: On a special configuration for the HRT conjecture, J. Fourier Anal. Appl.31(2025), no. 4, Paper No. 48, 2

2025
[15]

Vignon Oussa,Lean-certified four-point HRT results for three lattice points and one off-lattice point, 2026, arXiv:2604.21228v1

2026 arXiv
[16]

,One rogue point: The HRT conjecture beyond lattices, Book manuscript, 2026

2026
[17]

Rump,Verification methods: Rigorous results using floating-point arith- metic, Acta Numer.19(2010), 287–449

Siegfried M. Rump,Verification methods: Rigorous results using floating-point arith- metic, Acta Numer.19(2010), 287–449

2010
[18]

The mathlib Community,The Lean mathematical library, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Association for Computing Machinery, 2020, pp. 367–381

2020
[19]

Zeevi,Analysis of multiwindow Gabor-type schemes by frame methods, Appl

Meir Zibulski and Yehoshua Y. Zeevi,Analysis of multiwindow Gabor-type schemes by frame methods, Appl. Comput. Harmon. Anal.4(1997), no. 2, 188–221. Department of Mathematics, Bridgewater State University, Bridgewater, Massachusetts, USA Email address:voussa@bridgew.edu

1997

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.

[1] [1]

Jairo Bochi and Nicolas Gourmelon,Some characterizations of domination, Math. Z. 263(2009), no. 1, 221–231

work page 2009

[2] [2]

12699, Springer, 2021, pp

Leonardo de Moura and Sebastian Ullrich,The Lean 4 theorem prover and programming language, Automated Deduction—CADE 28, Lecture Notes in Computer Science, vol. 12699, Springer, 2021, pp. 625–635

work page 2021

[3] [3]

Ciprian Demeter,Linear independence of time frequency translates for special configu- rations, Math. Res. Lett.17(2010), no. 4, 761–779

work page 2010

[4] [4]

Ciprian Demeter and Alexandru Zaharescu,Proof of the HRT conjecture for(2, 2) configurations, J. Math. Anal. Appl.388(2012), no. 1, 151–159

work page 2012

[5] [5]

Linear dependence of time-frequency shifts of a Schwartz function

Markus Faulhuber, Philipp Petersen, Jordy Timo van Velthoven, and Felix Voigt- laender,Linear dependence of time–frequency shifts of a Schwartz function, 2026, arXiv:2608.05044v1; ancillary Arb code. AN INTRINSICALLY SUBCRITICAL FOUR-POINT COUNTEREXAMPLE 19

work page Pith review arXiv 2026

[6] [6]

Karlheinz Gröchenig,Foundations of time-frequency analysis, Applied and Numerical Harmonic Analysis, Birkhäuser, Boston, MA, 2001

work page 2001

[7] [7]

Christopher Heil,Linear independence of finite Gabor systems, Harmonic Analysis and Applications, Birkhäuser, Basel, 2006, pp. 171–206

work page 2006

[8] [8]

Christopher Heil, Jayakumar Ramanathan, and Pankaj Topiwala,Linear independence of time-frequency translates, Proc. Amer. Math. Soc.124(1996), no. 9, 2787–2795

work page 1996