Reasonable bounds for Restricted Polynomial Progressions in $\mathbb F^n_p$
Alex Burgin, Anastasios Fragkos, David Kruzel, Michael Lacey, Amelia Stokolosa
math.NT
Oct 9, 2026 · v1
math.CA math.CO
TL;DR
The paper's results were formalized in Lean by an AI agent, with a single admitted statement for the external inverse theorem (Theorem 1.4).
Abstract
Given an integer $k \geq 2$ and a prime $p$ large enough depending on $k$, we show that, if $A \subseteq \mathbb F^n_p$ does not contain a restricted polynomial progression of the form \begin{align*} x, x+\begin{pmatrix} y_1 \\ y_2 \\ \vdots \\ y_n \end{pmatrix}, x+\begin{pmatrix} y_1^2 \\ y_2^2 \\ \vdots \\ y_n^2 \end{pmatrix}, \ldots, x+\begin{pmatrix} y_1^{k-1} \\ y_2^{k-1} \\ \vdots \\ y_n^{k-1} \end{pmatrix}, \end{align*} where $x \in \mathbb F^n_p$ and $y \in \{0,2, 3, \ldots, M_k\}^n \backslash \{\vec{0} \}$, for some fixed $M_k$, then $A$ must have density bounded above by $\frac{C}{(\log^{(k^{O(k)})} n)^c}$, where $C, c>0$ only depend on $k$ and $p$. For $k\geq 4$, the best previously known bound came from the density Hales–Jewett theorem and was of inverse Ackermann type. The proof uses a recent inverse theorem for noise stability of Bhangale, Khot, Liu and Minzer, which arose in the study of constraint satisfaction problems. The main new ingredient is a proof that the underlying distribution counting restricted polynomial progressions does not admit a nontrivial abelian embedding.
Problem
The goal is quantitative density bounds for subsets of F_p^n that avoid restricted polynomial progressions x, x+y, x+y^2, ..., x+y^{k-1}, with steps y taken coordinatewise from {0,2,...,M_k}^n minus zero. For k>=4 the previous best bound came from density Hales–Jewett and was of inverse Ackermann type.
Approach
The argument applies the inverse theorem for noise stability of Bhangale, Khot, Liu and Minzer, which requires the counting distribution to admit no nontrivial abelian embedding. Any such embedding is first reduced to one into a cyclic group of prime order q. The case q=p is handled by a Vandermonde-type determinant over F_p[T]/(T^p-1), and the case q≠p by eigenspace decomposition of the translation operator. Stability bounds are then converted into density bounds via low-degree Fourier weight.
Results
Sets avoiding these progressions have density at most C/(log^{(k^{O(k)})} n)^c, with C and c depending only on k and p. The argument is formalized in Lean by an AI agent, except for the cited inverse theorem, which is admitted.
