Fitting arithmetic progressions into geometric progressions

by Srivatsa Chakravrathy Srinivas

This post aims to use a novel method using the package Haskell package SBV to solve an easy to state, but tricky problem.

Question. What is the longest non-trivial arithmetic progression that is a subset of a geometric progession?

This was an open question of K. Zarankiewicz which was solved by Schinzel in 1962. In this article, we re-write the tedious calculations in a Haskell program and extend the proof in the original article to extra cases. In order to formalize the question we first define a few notions

Definitions:

An arithemtic progression of length $k > 0$ is a sequence of $k+1$ elements $\xi_i \in \mathbb{C}$ such that for all $2 \leq i \leq k$ we have that $\xi_{i+1} - \xi_i = \xi_i - \xi_{i-1}$. It is non-trivial if $\xi_2 - \xi_1 \neq 0$
A geometric progression of length $k > 0$ is a sequence of $k+1$ elements $\xi_i \in \mathbb{C}$ such that for all $2 \leq i \leq k$ we have that $\xi_{i+1}/\xi_i = \xi_i/\xi_{i-1}$.
We define $\boldsymbol{P(k)}$ to be the following statement: $\exists$ an arithmetic progression of length $k$, $[\xi_1, \ldots, \xi_{k+1}]$, and a geometric progression of length $r$, $[\rho_1, \ldots, \rho_{r+1}]$, such that the set of terms in the aforementioned arithmetic progession are a subset of the terms of the aforementioned geometric sequence, ie $\{\xi_i\} \subset \{\rho_i\}$
For $l,m,n \in \mathbb{N}_{\geq 0}$ we define $p_{l,m,n} = x^l - 2x^m + x^n \in \mathbb{Z}[x]$

The question can be reframed as the following: What is the largest $k$ such that $P(k)$ is true. It makes sense check some cases where $k$ is small.

Case $k = 1$: This is the easiest case. Take the geometric and arithmetic progression to be the sequence $[2,4]$
Case $k = 2$. This case is slightly more difficult. We let $\xi \in \mathbb{C}$ and force $\xi$ to have the following constraints \[ \xi^3 - \xi^1 = \xi^1 - \xi^0 \]Then we will have that $[1,\xi,\xi^3]$ forms an arithmetic progression of length $2$ that is a subset of the geometric progression $[1,\xi,\xi^2,\xi^3]$. We find all such $\xi$ by solving $x^3 - 2x^2 + 1 = 0$. The solutions are \[ x = 1, \frac{1+\sqrt{5}}{2}, \frac{1-\sqrt{5}}{2}\] Thus if $\xi \neq 1$ and is chosen from above then $[1,\xi,\xi^3]$ is a non-trivial arithemtic progression contained in a geometric progression.
Case $k = 3$. Note that $P(3)$ is equivalent to the following: There exists an $\xi \in \mathbb{C}$ and $a,b,c,d \in \mathbb{Z}$ such that \[x^c - x^b = x^b - x^a\] \[x^d - x^c = x^c - x^b\] Thus we have that $[\xi^a,\xi^b,\xi^c,\xi^d]$ is an arithmetic progression iff $\xi$ is a root of the two polynomials $p_{c,b,a}$ and $p_{d,c,b}$. For the rest of the article we consider Case $k = 3$.

(Longest a.p in a g.p) If there is an arithemtic progression of length at least $3$ that is a subset of $(\xi^i)_{i \in \mathbb{Z}}$ then we have that $\xi = 0$ or $\xi$ is a root of unity (i.e, $\exists m \in \mathbb{N}$ such that $\xi^m = 1$)

1. Converting the problem to something that a computer can solve

We now define the “reverse” of a polynomial.

Definition. Given a polynomial $p \in \mathbb{Z}[x]$, we define the reversal of $p$ by \[p^\dagger = x^{\deg p}p(1/x)\]

That is if \[p(x) = \sum_{i = 0}^n a_i x^i\] Then \[p^\dagger(x) = \sum_{i = 0}^n a_{n-i}x^i\] We note that the reversal has the following property: $(pq)^\dagger = p^\dagger q^\dagger$. Thus we have the following lemma

Lemma. $p$ is an irreducible polynomial iff $p^\dagger$ is an irreducible polynomial

We will now present a Lemma that will allow us to factor $p_{a,b,c}(x)$

Definition. A polynomial $p \in \mathbb{Z}[x]$ is said to be uniquely positive if for every $q \in \mathbb{Z}[x]$ such that $pp^\dagger = qq^\dagger$ we have that $q = \varepsilon p$ or $q = \varepsilon p^\dagger$, where $\varepsilon = \pm 1$
Definition. A polynomial $p \in \mathbb{Z}[x]$ is said to be symmetric if $p = p^\dagger$. The symmetric part, s, of a polynomial $p$ is the maximal symmetric divisor of $p$. We define the antisymmetric part of $p$ to be $p/s$.
Lemma (Uniquely positive form). A polynomial $p \in \mathbb{Z}[x]$ is uniquely positive iff it can be written as $p = sf$ where $s = s^\dagger$, $f$ is irreducible and $f \neq f^\dagger$ or $f = 1$

Proof (Uniquely positive form) We write $p = \pi_1 \cdots \pi_n$ where $\pi_i$ are irreducible and $\pi_1 , \ldots, \pi_k$ are symmetric. If $k \leq n-2$ then we have that on setting $p_1 = \pi_1\cdots \pi_{n-2} \pi_{n-1} \pi_n^\dagger$, we note that $p_1 \neq p$ but $p_1p_1^\dagger = pp^\dagger$. Thus if $p$ is to be uniquely symettric then we have that $k \geq n-1$ and so $p = sf$ where $s$ is symmetric and $f$ is irreducible. We note that if $q = \mu_1 \cdots \mu_l$ where $\mu_i$ are irreducible, then we have that $pp^\dagger = \pm qq^\dagger$ if and only if $l = n$ and there is a permuations $\sigma$ of $\{1,\ldots,n\}$ such that for all $i$ we have that either $\pi_i = \pm \mu_{\sigma(i)}$ or $\pi_i = \pm \mu_{\sigma(i)}^\dagger$. Therefore if $p = sf$ where $s$ is symmteric and $f$ is irreducible then we have that for all $i \leq n-1$ we have that $\pi_i = \pm \mu_{\sigma(i)}$. Therefore the only possiblilites for $q$ are $\pm \pi_1 \cdots \pi_{n-1}\pi_n$ or $\pm \pi_1 \cdots \pi_{n-1}\pi_n^\dagger$. Thus $q = \pm p$ or $q = \pm p^\dagger$.

$\blacksquare$

Thus if we can show that a polynomial is uniquely positive, and we know it’s “symmetric part” (that is the maximal divisor $s$ that satisfies $s = s^\dagger$). Then we have factorized the polynomial. This will help us factor $p_{a,b,c}$.

Lemma (Symmetric part of $\boldsymbol{p_{a,b,c}}$). Let $a,b,c \in \mathbb{N}_{\geq 0}$ be such that $a = b = c$ does not hold. The symmettric part of $p_{a,b,c}$ is $s = x^{e_3}(x^{\gcd(e_1-e_3,e_2-e_3)} - 1)^{e_4}$ where $[e_1,e_2,e_3]$ is $[a,b,c]$ sorted in descending order and $e_4 = 1$ if $e_1 - e_2 \neq 2(e_2 - e_3)$ and $e_4 = 2$ otherwise

Proof (Symmetric part of $\boldsymbol{p_{a,b,c}}$). Since $x^{e_3}$ is symmetric, we only need to find the symmetric part of $p_{a,b,c}/x^{e_3}$. We set $p' = p_{a,b,c}/x^{e_3}$, $n = e_1 - e_3$ and $m = e_2 - e_3$. Note that $n > m$. Before we proceed, we would like to mention that the case where $2m = n$ is trivial and hence we may assume that $2m \neq n$. We can also infer from the hypothesis that $n > 0$. We first prove the following claim:

Claim. $\xi$ is a root of the symmetric part of $p'$ iff $\xi$ is a root of $x^{\gcd(m,n)}-1$. Furthermore the multiplicity of the root $\xi$ in $p'$ is 1.

Proof of Claim.

Case $p' = x^n - 2x^m + 1$: We know that $p'^\dagger(x) = x^n - 2x^{n-m} + 1$. Now if $p'(\xi) = p'^\dagger(\xi) = 0$, we can deduce that $\xi^{n-m} = \xi^{m}$. Combining this fact with $p'(\xi) = 0$ (writing $n$ as $n-m+m$) gives us that $\xi^m = 1$, and $\xi^n = 1$ readily follows after. Thus $\xi$ is a root of $x^{\gcd(m,n)}-1$. Conversely, every root of $x^{\gcd(m,n)} -1$ is a root of $p'$. Note that $\frac{dp'}{dx}(\xi) = (n-2m)\xi^{-1} \neq 0$. Thus we have proven the claim.
Case $p' = -2x^n + x^m + 1$: In this case $p'^\dagger(x) = x^n + x^{n-m} - 2$. Let $p'(\xi), p'^\dagger(\xi) = 0$. If $|\xi| > 1$ then \[ \begin{aligned} 2|\xi|^n &\geq 2|\xi|^m \\ \implies 2|\xi|^n &\geq |\xi|^m + 1 \\ \implies 2|\xi|^n &\geq |\xi^m + 1| \end{aligned} \] Contradicting $p'(\xi) = 0$. Thus $|\xi| \leq 1$. Now since, $\xi^n + \xi^m -2 = p'^\dagger(\xi) = 0$, the triangle inequality implies that $\xi^n = \xi^m = 1$. And thus, $\xi$ is a root of $x^{\gcd(m,n)} - 1$. Conversely, every root of $x^{\gcd(m,n)} -1$ is a root of $p'$. Note that $\frac{dp'}{dx}(\xi) = (m - 2n)\xi^{-1} \neq 0$. Thus we have proven the claim.
Case $p' = x^n + x^m - 2$: Since the symmetric part of $p'$ is the same as that of the symettric part of $p'^\dagger = -2x^n + x^{n-m} + 1$, we have that the every root of the symmetric part of $p'$ is a root of $x^{\gcd(n,n-m)} - 1 = x^{\gcd(m,n)}-1$. Conversely, every root of $x^{\gcd(m,n)} -1$ is a root of $p'$. Note that $\frac{dp'}{dx}(\xi) = (n + m)\xi^{-1} \neq 0$ and thus we have proven the claim.

$\blacksquare$

The above claim combined gives us that the symmetric part of $p'$ is $x^{\gcd(m,n) - 1}$. $\blacksquare$

In order to use the above information to factor $p_{a,b,c}$ we need to prove that $p_{a,b,c}$ is uniquely postive. We can now jump into the realm of computation! (Technically, by the Curry-Howard correspondence, the reader understanding the above proof would also count as computation)

2. Opening the floodgates of computation

The following is based on a trick of Wilhelm Ljunggren. We now define the coefficient operator

Definition. We define the coeffcient operator for an $m \in \mathbb{Z}$ as follows, given any polynomial $p(x) = a_nx^n + \cdots + a_0$ we define \[ [x^m]p(x) = a_m\] where $a_m = 0$ if $m <0$ or $m > n$

Lemma. Let $p(x) = a_nx^n + \cdots + a_0$. Then $[x^n] pp^\dagger (x) = \sum_{i = 0}^n a_i^2$

Proof. \[ \begin{aligned} {}[x^n]pp^\dagger(x) &= \sum_{\substack{0 \leq i,j \leq n \\i+j = n}} ([x^i]p(x))([x^j]p^\dagger(x)) \\ &= \sum_{i = 0}^n a_i(a_{n-(n-i)}) \\ &= \sum_{i = 0}^n a_i^2 \end{aligned} \] $\blacksquare$

Note that if $[e_1,e_2,e_3]$ is $[a,b,c]$ sorted in descending order then we have that \[ [x^{e_3}] p_{a,b,c}p_{a,b,c}^\dagger (x) = \begin{cases} 0 & e_3 = e_1 \\ 2 & e_3 = e_2 \text{ or } e_2 = e_1 \\ 6 & e_3 > e_2 > e_1 \\ \end{cases} \] In the case $e_3 = e_1$, $p_{a,b,c}(x) = 0$ and in the case $e_3 = e_2 \, \text{or} \, e_2 = e_1$ we have that $p_{a,b,c}(x) = (-1)^{e_4}(x^{e_3} - x^{e_1})$ where $e_4 = 1$ if $e_3 = e_2$ and $0$ otherwise. Thus the only case that we have not fully factored $p_{a,b,c}$ is when $e_3 > e_2 > e_1$. The rest of the section will focus on the last case.

Thus, the above lemma says that if $qq^\dagger = p_{a,b,c}p_{a,b,c}^\dagger$ then we must have that sum of squares of the coefficients of $q$ must be $6$. This means that there are at most finitely many possibilities for the coefficients of $q$. We can now get to work!

Lemma If $b > \max\{a,c\}$ or $b < \min\{a,c\}$ then we have that $p_1 = p_{a,b,c}/x^{\min\{a,b,c\}}$ is uniquely positive

Proof. Suppose that $b > \max \{a,c\}$ and $p_1p_1^\dagger = \pm qq^\dagger$ where and $p = p_{a,b,c}$. Without loss of generality we may assume that $a \leq c$. Then we must have that $-2 = [x^{2b}]p_1(x)p_1^\dagger(x) = [x^{2b}] q(x)q^\dagger(x) = [x^b]q(x)[x^0]q(x)$. This means that either $[x^0]q(x) = \pm 2$ or $[x^b]q(x) = \pm 2$. In either case, since the square of the coefficients of $q(x)$ have to add to be $6$, this forces $q(x) = \pm 1(-2x^{b-a} + x^{c-a} + 1)$ or $q(x) = \pm 1(x^{b-a} + x^{c-a} - 2) = p_1^\dagger (x)$. Thus we have shown that $p_1$ is uniquely positive in the case of $b > \max \{a,c\}$. In the case of $b < \min \{a,c\}$ we note that $p_1^\dagger$ falls into the previous case, therefore we are done. $\blacksquare$

So the only interesting case is when $a > b > c$. Let $p_{m,n}(x) = x^n - 2x^m + 1$, where $n > m$. Suppose that $qq^\dagger(x) = p_{m,n}p_{m,n}^\dagger(x)$. Then we know that if $q(x) = \sum_{i = 1}^n a_i x^i$, it must be that $\sum_{i = 1}^n a_i^2 = 6$. It is easy to see that if for some $i$ we have that $a_i = \pm 2$ then it must be the case that $q(x) = \pm p_{m,n}(x)$ or $q(x) = \pm p_{m,n}^\dagger(x)$. Therfore the only interesting case is when $q(x) = \sum_{i = 1}^6 a_ix^{k_1}$ where $a_i = \pm 1$. We will follow this case for the rest of the article.

3. Putting the computation in a computer

We want to find the $a_i,k_i,n,m$ such that $p_{m,n}(x)p_{m,n}^\dagger(x) = q(x)q^\dagger(x)$ where $p_{m,n} = x^n - 2x^m + 1$, $q(x) = \sum_{i = 1}^6 a_ix^{k_i}$, $a_i = \pm 1$ and $m < n$

Definitions.

An a_expr and b_expr are defined as follows:
```
a_expr :: symbol 
	| n ∈ ℤ
	| a_expr + a_expr
	| a_expr * a_expr
b_expr :: True 
	| False
	| a_expr < a_expr
	| a_expr > a_expr
	| a_expr = a_expr
	| b_expr && b_expr
	| b_expr || b_expr
	| not b_expr
```
Which means that you build an a_expr using symbols, integers and the operations $+$ and $*$. A b_expr is built using the values True and False, a_exprs compared using relations and the boolean AND (&&), OR (||). Examples of an a_expr would be $x$, $1 + y$ and an example of a b_expr is $x > 1+y$
A b_expr containing symbols $x_1,\ldots,x_n$, denoted by $B(x_1,\ldots,x_n)$, is said to be satisfiable if the statement $\exists x_1, \ldots ,x_n \in \mathbb{Z}. B(x_1, \ldots, x_n)$ is True and is said to be unsatisfiable otherwise.
An integer solver is a function whose input is a b_expr and whose output is either Nothing, or whether the b_expr is satisfiable or unsatisfiable. It is unfortunately true that determining the satisfiability of a b_expr is undecidable. That is why we allow the solver to “time out” on occasion.
Given a list of b_exprs $\text{ls} = [B_1(x_{11},\ldots,x_{1n_1}), \ldots, B_m(x_{m1},\ldots,x_{mn_m})]$ we define \[ B_{\text{ls}} := B_1(x_{11},\ldots,x_{1n_1}) \,\&\&\, \ldots \,\&\&\, B_m(x_{m1},\ldots,x_{mn_m}) \]
We say that a b_expr, $B(x_1,\ldots,x_n)$ is provable if, $\text{not } B(x_1,\ldots,x_n)$ is unsatisfiable. Given a b_expr $B(x_1,\ldots,x_n)$, and a list of b_exprs $\text{ls}$ we say that $B(x_1,\ldots,x_n)$ is satisfiable (resp. unsatisfiable, provable) with constraints $\boldsymbol{\text{ls}}$ if \[B(x_1,\ldots,x_n) \,\, \&\& \,\, B_{\text{ls}}\] is satisfiable (resp. unsatisfiable, provable).

How can we construct an integer solver? That is a topic for another day! Luckily there are many integer solvers packaged into more general automated problem solvers called SMT (Satisfiable Modulo Theory) solvers. The Haskell package SBV allows one to construct b_exprs and query an SMT solver to return one of the following: time out, satisifiable or unsatisfiable. We will be using the cvc5 solver in this project.

Definitions.

A symbolic polynomial is a pair $(p,\text{ls})$ where $p$ is a list of the form $[(a_n,k_n), \ldots, (a_0,k_0)]$ (called the body), where the $a_i,k_i$ are b_exprs and $\text{ls}$ is a list of b_exprs that is satisfiable. It said to be in normal form if $k_i < k_j$ is provable with constraints $\text{ls}$ for any $i < j$. We can write a body $p = [(a_i,k_i)]$ in the following notation \[ \sum_{i = 1}^n a_ix^{k_i} \]
We say that a symbolic polynomial with body $[(a_0,k_0), \ldots, (a_n,k_n)]$ depends on $(z_1,\ldots,z_r)$ if we have that any variable that appears in $a_i$ or $k_i$ appears in the tuple $(z_1,\ldots,z_r)$

Given a symbolic polynomial $(p,\text{ls})$ that depends on $(z_1,\ldots,z_r)$ we want to determine if there are any solutions in $(z_1,\ldots,z_r)$ to the equation \[ \exists z_1,\ldots,z_r \in \mathbb{Z}. \, \sum_{i = 1}^n a_{i}x^{k_i} = 0 \] with constraints in the constraint list $\text{ls}$. If $(p,\text{ls})$ is in normal form then obviously the above is equivalent to solving for \[ \exists z_1,\ldots,z_r \in \mathbb{Z}. \, \forall 1 \leq i \leq n. a_i = 0 \] with constraints $\text{ls}$. But what if $(p,\text{ls})$ is not in normal form? Then, there are multiple possibilities as to how to “collect terms”. For example, $a_1x^{k_1} + a_2x^{k_2}$ is equal to $(a_1 + a_2)x^{k_1}$ if the term $k_1 = k_2$ appears in the constraint list. So, how can we know what expressions to equate to 0 in order to determine if a symbolic polynomial can be equal to 0? We construct a term that accomplishes that called checkZeroSat in this repository

Lemma (Algorithm) Given a symbolic polynomial $p$, the term runSMT (p >>= checkZeroSat) returns either an SMT time out, prints out a solution if there exists $(a_i,k_i)$ such that $\sum_{i = 1}^n a_ix^{k_i} = 0$ or “Failure” if there does not exist $(a_i,k_i)$ such that $\sum_{i = 1}^n a_ix^{k_i} = 0$

4. Using the algorithm on our problem

Now we consider the symbolic polynomial \[ r(x) = p(x)p^\dagger(x) - q(x)q^\dagger(x) \] where $p(x) = x^n - 2x^m + 1, q(x) = \sum_{i = 1}^6 a_ix^{k_i}$ with constraint list \[ \text{ls} = [ a_i = \pm 1, k_i < k_{i+1}, n > 2*m, k_1 = 0 ] \] We may take the assumption $n > 2m$ because, in the previous section we assumed that $n > m, n \neq 2m$ and since $p^\dagger_{m,n}(x) = p^\dagger_{n-m,n}(x)$ without loss of generality, we may take $n > 2m$. We can take $k_1 = 0$ to be an assumption since $x \nmid p(x)p^\dagger(x)$. So now, all we have to check is that if there are solutions in $(a_i,k_i),n,m$ to \[ r(x) = 0 \] with constraint list $\text{ls}$. Okay, let us try and see if $r(x) = 0$ is satisfiable


ghci> runSMT (r >>= checkZeroSat)
SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("a0",1 :: Integer),("a1",-1 :: Integer),("a2",-1 :: Integer),("a3",-1:: Integer),("a4",1 :: Integer),("a5",1 :: Integer),("k0",0 :: Integer),("k1",1 :: Integer),("k2",4 :: Integer),("k3",5 :: Integer),("k4",6 ::Integer),("k5",7 :: Integer),("p0",0 :: Integer),("p1",2 :: Integer),("p2",7 :: Integer)], modelUIFuns = []}

Where $p2 = n, p1 = m$. So that tells us that there is a solution to $r(x) = 0$, namely when $n = 7,m = 2$. This is because \[ x^{7k} - 2x^{2k} + 1 = (x^k-1)(x^{3k}+x^{k}+1)(x^{3k}+x^{2k}-1) \] and hence when $7m = 2n$, $p_{m,n}$ is not uniquely positive. Now let us add the constraint $7*m \neq 2*n$ to the constraint list. Then we get


ghci> runSMT (rWithConstraint >>= checkZeroSat)
"Failure"

So if $7m \neq 2n$ and $n > 2m$ we have that $p_{m,n}$ is uniquely positive. By symmetry this gives us that if $2m \neq n$ and $7m \neq 2n$ and $7m \neq 5n$ then $p_{m,n}$ is uniqely positive. We thus deduce the following theorem

Theorem (Classifying $p_{m,n}$) Let $p_{a,b,c}(x) = x^a - 2x^b + x^c$, with $a,b,c \in \mathbb{Z}$ all being different. Let $[e_1,e_2,e_3]$ be the list $[a,b,c]$ sorted in descending order. Set $n = e_1 - e_2$, $m = e_1-e_3$. Then we have that $p_{a,b,c}(x) = x^{e_3}(x^{\mathrm{gcd}(m,n)}-1)^\epsilon f$ where

Case $p_{a,b,c}(x) \neq x^{e_3}(x^n-2x^m +1)$: $\epsilon = 1$, $f$ is irreducible and antisymmetric
Case $p_{a,b,c}(x) = x^{e_3}(x^n-2x^m +1)$, $m \neq 2n$, $7m \neq 2n$, $7m \neq 5n$: $\epsilon = 1$, $f$ is irreducible and antisymmetric
Case $p_{a,b,c}(x) = x^{e_3}(x^n-2x^m +1)$, $m \neq 2n$, $7m = 2n$: $\epsilon = 1$, $f = (x^{3k}+x^k+1)(x^{3k}+x^{2k}-1)$
Case $p_{a,b,c}(x) = x^{e_3}(x^n-2x^m +1)$, $m \neq 2n$, $7m = 5n$: $\epsilon = 1$, $f = (x^{3k}-x^k-1)(x^{3k}+x^{2k}+1)$
Case $p_{a,b,c}(x) = x^{e_3}(x^n-2x^m +1)$, $m = 2n$: $\epsilon = 2$, $f = 1$.

5. Using the result to finish the problem

Using the Main Theorem, one can now show that the following is true

Lemma (Non-symmetric parts are coprime). Let $n > m > 0$, $k > 0$ and

$\alpha_{m,n} = \frac{x^n - 2x^m + 1}{x^{\mathrm{gcd}(m,n)}-1}$ where $7m \neq 2n$ or $7m \neq 5m$
$\beta_{m,n} = \frac{- 2x^n + x^m + 1}{x^{\mathrm{gcd}(m,n)}-1}$
$\gamma_{m,n} = \frac{x^n + x^m - 2}{x^{\mathrm{gcd}(m,n)}-1}$
$\mu_k = x^{3k} + x^k + 1$
$\nu_k = x^{3k} + x^{2k} - 1$
$\mu_k^\dagger$
$\nu_k^\dagger$

Then we have that all the polynomials above are distinct (upto multiplication by a unit) and irreducible over $\mathbb{Z}$

Proof. Unfortunately, the proof of this fact boils down to a lot of case checking. Using the exact same technique in the previous section, we can prove that $\mu_k$ and $\nu_k$ are irreducible. It is easy to see that any $\beta_{m,n}$ are distinct to polynomials from any other family beacuse it’s top coefficient is $2$. Similarlyf or $\gamma_{m,n}$ since we have that the top coefficient of $\gamma_{m,n}^\dagger$ is $2$. Therefore the annoying cases are checking that two polynomials from the same family are distinct and that $\alpha_{m,n}$ are distinct from the $\mu_k, \nu_k, \mu_k^\dagger, \nu_k^\dagger$. We will use the algorithm to prove that these polynomials are not equal in any case. The code for the proofs are found in the same repository.

$\blacksquare$

(Final Lemma) For any $a,b,c,d\in \mathbb{N}_{\geq 0}$ such that $|\{a,b,c,d\}| = 4$, we have that \[ \mathrm{gcd}(p_{a,b,c}(x),p_{b,c,d}(x)) = \mathrm{gcd}(x^{e}(x^{\mathrm{gcd}(m_0,n_0)}-1)^{\epsilon_0},x^{f}(x^{\mathrm{gcd}(m_1,n_1)}-1)^{\epsilon_1}) \] where $[k_1,k_2,k_3],[l_1,l_2,l_3]$ are the lists $[a,b,c],[b,c,d]$ sorted in descending order, $m_0 = k_1 - k_2, n_0 = k_1-k_3$, $m_1 = l_1-l_2, n_1 = l_1-l_3$, $e = k_3, f = l_3$ and \[ \epsilon_i = \begin{cases} 1 & \, \text{if $2m_i \neq n_i$} \\ 2 & \, \text{if $2m_i = n_i$} \end{cases} \]

Proof. We know that the gcd of two polynomials $f,g \in \mathbb{Z}[x]$ is the product of the gcd of their symettric parts and their antisymettric parts. Therefore, by the above Lemma (Non-symmetric parts are coprime) we know that the gcd of the antisymmetric parts of $p_{a,b,c}$ and $p_{b,c,d}$ is not $1$ if and only if we have that there exists a $\gamma \in \mathbb{Z}$ such that $[k_1 + \gamma,k_2 + \gamma,k_3 + \gamma] = [l_1,l_2,l_3]$. But since we know that both lists contain a sublist corresponding to the list $[b,c]$ sorted in descending order, we must have that for some $i,j \in \{1,2,3\}$ that $[k_i + \gamma, k_j + \gamma] = [k_i,k_j]$. Thus $\gamma = 0$ and we deduce that for all $i \in \{1,2,3\}$ that $k_i = l_i$. This gives us that $|\{a,b,c,d\}| < 4$, a contradiction

$\blacksquare$

Thus by the above theorem we can finally conclude that if $(\xi^a)_{a \in \mathbb{Z}}$ contains a four term arithmetic progresison, then it must be that $x = 0$ or that $x$ is a root of unity.