What was already known
Earlier root-of-unity constructions supplied cycling regions, and mixed-mode feasibility was already known. The paper credits its Fourier analysis, one-dimensional construction and non-acceleration argument to the human authors; those are not attributed to AI here.
AI involvement
The authors explicitly identify Example 3.2 and the Section 5 counterexample as AI-generated and independently verified by them. They separately credit the main Fourier analysis and rotation/projection idea to themselves. This supports central AI construction of these witnesses, not the whole paper.
Importance
Gives explicit witnesses that ordered root-of-unity cycling is too narrow and that even all pure modes miss some higher-dimensional cycles.
Limitations
Only the two disclosed AI-generated examples are retained. The general one-dimensional non-acceleration theorem is not an AI discovery in this record. Lean checks their exact certificates, but the mixed-condition sufficiency theorem is outside the formalization. The authors credit Chung-En Tsai with an independent concurrent similar four-dimensional example; priority is not exclusive.
Technical verification
The named authors report verifying both examples. The accompanying Lean development checks Example 3.2 and the Section 5 exact certificate: nine mixed inequalities, the uniform exclusion for large periods and thirteen finite algebraic cases. Existence of the four-dimensional cycle also uses the paper’s human-checked sufficiency argument, which is not formalized.
Independent checking
The AI declaration reports completed human verification; Sections 3 and 5 explain the witnesses and sufficiency argument
- Checker
- Konstantinos Fotopoulos, Michael Helcig, Karl Deck and Jannis Alsbach
- Scope
- Two AI-generated heavy-ball counterexamples separate cycling regions for smooth strongly convex functions. Example 3.2 uses κ=4/5, β=17/20 and Lγ=18/5 to admit a primitive (K,m)=(5,2) cycle while excluding all ordered m=1 modes. Section 5 uses L=1, (κ,β,γ)=(531/10000,4879/10000,32829/12500) and a ten-step mixture of modes 2 and 3 with weights 137/500 and 363/500: it supports a four-dimensional cycle but excludes every pure root-of-unity mode.
- Basis
- Reported by the linked checker
Independent checking
Exact arithmetic inequalities, uniform large-period exclusion and thirteen finite algebraic cases; mixed-condition sufficiency excluded
- Checker
- Authors’ Lean 4 / Mathlib development
- Scope
- Example 3.2 and Section 5 numerical and pure-mode exclusion certificates
- Basis
- Reported by the linked checker
Human understanding
Fotopoulos, Helcig, Deck and Alsbach explain the Fourier-mode conditions, the two-plane mixture, all-period exclusion and the distinction from their human-origin non-acceleration proof.
Correction and publication history
Added a reviewed, scoped central-AI contribution with checking and attribution limits.
Read this published revision