2.1 Bounded arithmetic and the theories in question

In this section, we recall basic facts about the theories relevant to our formalization. We refer the reader interested in a comprehensive treatment of bounded arithmetic to [Reference Krajíček15].

The minimal language we consider is Buss’ language $L_{S_2}$ [Reference Buss3] used in the original definition of the theory $S^1_2$ (see below). The language $L_{S_2}$ consists of the nonlogical symbols $\{0,S,+,\cdot , \leq , \#, \left \lfloor {x/2} \right \rfloor , {\lvert {x} \rvert }\}$ and all the usual logical symbols. The symbols $0, S,+,\cdot , \leq $ are the zero constant, the successor function, addition, multiplication, and the less-than-or-equal-to relation. The intended meaning of $\left \lfloor {x/2} \right \rfloor $ is to divide by two and round down, and $|x|$ is $\lceil \text {log}\,_2 (x+1) \rceil $ , which is the length of the binary representation of x. We define $x \# y=2^{|x| \cdot |y|}$ . The behavior of these symbols is axiomatized by the 32 universal axioms of $\text {BASIC}$ (see [Reference Buss3, Section 2.2]). As we will only consider logarithms base 2, from now on, by $\text {log}\, x$ , we mean $\text {log}\,_2 (x)$ . Denote $S(0)$ by $1$ . The $L_{S_2}$ -terms and $L_{S_2}$ -formulas are defined as usual.

A bounded quantification of the free variable x in an $L_{S_2}$ -formula $\varphi (x)$ is either of the following

$$ \begin{align*} &(\forall x \leq t)(\varphi(x))\equiv(\forall x)(x\leq t \to \varphi(x))\\ &(\exists x \leq t)(\varphi(x))\equiv(\exists x)(x\leq t \land \varphi(x)), \end{align*} $$

where t is an $L_{S_2}$ -term that does not contain x. We call the quantifiers of the above form bounded. We say a quantifier is sharply bounded if it is bounded and the term t is of the form ${\lvert {s} \rvert }$ for some term s. A (sharply) bounded formula in the language $L_{S_2}$ is simply a formula in which every quantifier is (sharply) bounded. The set of all bounded formulas is denoted $\Sigma ^b_\infty $ . An $L_{S_2}$ -formula is $\Sigma ^b_0=\Pi ^b_0$ if all its quantifiers are sharply bounded. An $L_{S_2}$ -formula is $\Sigma ^b_1$ (resp. $\Pi ^b_1$ ) if it is constructed from sharply bounded formulas using conjunction, disjunction, sharply bounded quantifiers and existential (resp. universal) bounded quantifiers.

The theory $S^1_2$ is axiomatized over BASIC by the polynomial induction schema $\Sigma ^b_1$ -PIND for any $\Sigma ^b_1$ -formula $\varphi $ :

$$\begin{align*}\varphi(0) \wedge \forall x (\varphi(\left \lfloor {x/2} \right\rfloor) \to \varphi(x)) \to \varphi(a), \end{align*}$$

or alternatively by the length minimization schema $\Sigma ^b_1$ -LMIN:

$$\begin{align*}\varphi(a) \to (\exists x\leq a)(\forall y \leq a)(\varphi(x) \land ({\lvert {y} \rvert}<{\lvert {x} \rvert} \to \lnot \varphi(y))\end{align*}$$

for any $\Sigma ^b_1$ -formula $\varphi $ , or by the length maximization schema $\Sigma ^b_1$ -LMAX:

$$\begin{align*}\varphi(0) \to (\exists x \leq a)(\forall y \leq a)(\varphi(x)\land ({\lvert {x} \rvert}<{\lvert {y} \rvert} \to \lnot \varphi(y))) \end{align*}$$

for any $\Sigma ^b_1$ -formula $\varphi $ . The theory $T_2$ is axiomatized over BASIC by the induction schema $\Sigma ^b_{\infty }$ -IND:

$$\begin{align*}\varphi(0) \wedge \forall x (\varphi(x) \to \varphi(x + 1)) \to \forall x \varphi(x). \end{align*}$$

for any $\Sigma ^b_{\infty }$ -formula, or equivalently bounded formula $\varphi $ .

Throughout this paper, we shall use the richer language of Cook’s theory $\mathrm {PV}$ [Reference Cook7] and of the theory $\mathrm {PV}_1$ [Reference Krajíček, Pudlák and Takeuti16], which contains function symbols for every polynomial-time algorithm. In particular, this language includes $L_{S_2}$ . With a slight abuse of notation, we also use $\mathrm {PV}$ to refer to this richer language. We will simply refer to these function symbols for polynomial-time algorithms as $\mathrm {PV}$ -symbols. We shall sometimes treat them as predicates, which we call $\mathrm {PV}$ -predicates. The intended meaning of a $\mathrm {PV}$ -predicate is that a corresponding $\mathrm {PV}$ -symbol for the characteristic function of the predicate outputs $1$ . The definitions of $\Sigma ^b_1$ , $\Pi ^b_1$ , and $\Sigma ^b_\infty $ can be extended to this new language by allowing the terms and open formulas to be in $\mathrm {PV}$ . These classes of formulas are called $\Sigma ^b_1(\mathrm {PV})$ , $\Pi ^b_1(\mathrm {PV})$ , and $\Sigma ^b_\infty (\mathrm {PV})$ , and the expanded theories $S^1_2(\mathrm {PV})$ and $T_2(\mathrm {PV})$ . However, with a slight abuse of the notation, we use $\Sigma ^b_1$ , $\Pi ^b_1$ , and $\Sigma ^b_\infty $ , $S^1_2$ , and $T_2$ .

The weakest theory we consider is $\mathrm {PV}_1$ , first defined in [Reference Krajíček, Pudlák and Takeuti16] as a conservative extension of Cook’s equational theoryFootnote ² $\mathrm {PV}$ [Reference Cook7]. The theory $\mathrm {PV}_1$ , a universal first-order theory, formalizes polynomial-time reasoning in the language of $\mathrm {PV}$ . It is shown in [Reference Krajíček15] that $\mathrm {PV}_1$ proves $\Sigma ^b_0$ -IND. We say that the formula A is $\Delta ^b_1$ -definable in a theory R if there are formulas $B \in \Sigma ^b_1$ and $C \in \Pi ^b_1$ such that $A \leftrightarrow B$ and $A \leftrightarrow C$ are provable in the theory R. Every $\mathrm {PV}$ -function can be $\Delta ^b_1$ -defined in $S^1_2$ , hence we can see $S^1_2$ as an extension of $\mathrm {PV}_1$ (see [Reference Buss3]). Also, using Buss’ witnessing theorem [Reference Buss3], we can see that $S^1_2$ is $\forall \Sigma ^b_1$ -conservative over $\mathrm {PV}_1$ . Therefore, when we want to prove a $\forall \Sigma ^b_1$ -formula in $\mathrm {PV}_1$ , we can prove it in $S^1_2$ . As mentioned earlier, we assume that $S^1_2$ is in the language $\mathrm {PV}$ . To prove the existence of prime factorization of numbers, it seems to be necessary to work in $S^1_2$ (see [Reference Jeřábek10]).

Let us define an axiom schema, which we will use later. The injective weak pigeonhole principle $\mathrm {iWPHP}(\mathrm {PV})$ is the axiom schema

$$\begin{align*}a>0 \to \big((\exists x <2a)(f(x)\geq a) \lor (\exists x< x' < 2a)(f(x)=f(x'))\big) \end{align*}$$

for each $\mathrm {PV}$ -symbol f. We will introduce two additional axiom schemata, the Generalized Fermat’s Little Theorem ( $\text {GFLT}$ ) and the Root Upper Bound ( $\mathrm {RUB}$ ), once we have defined all the required notions. The axiom $\text {GFLT}$ is treated in Definition 2.2, and the axiom $\mathrm {RUB}$ and the resulting theory $S^1_2+\mathrm {iWPHP}+ \mathrm {RUB}$ are treated in Section 4.3.

Another essential theory for us is the theory $T^{\text {count}}_2$ . It consists of the theory $T_2(\mathrm {PV})$ with its language extended by a recursively defined family of counting functions for each $\Sigma ^b_\infty $ -formula A. Then, for each bounded formula, it contains the first level counting functions, and so on. We will not work with this theory directly. Instead, we will consider $\Sigma ^b_\infty $ -consequences of the theory $\text {VTC}^0_2$ which are fully conservative over $T^{\text {count}}_2$ [Reference Krajíček15, essentially Lemma 13.1.2].

Let us now define the theory $\text {VTC}^0_2$ . First, the theory $V^0_2$ is a two-sorted extension of $T_2$ , where the first sort is the “number sort” denoted by lowercase variables $x, y, \ldots $ as in $T_2$ , and the new “set sort” corresponds to binary strings whose bits are indexed by the number sort and is denoted by uppercase variables $X, Y, \ldots $ . The language of $V^0_2$ is extended by an equality symbol for the set sort, the elementhood relation $x\in X$ between the number sort on the left and the set sort on the right, and the length symbol ${\lvert {X} \rvert }$ , which takes as an input an element of the set sort and outputs an element of the number sort. The intended meaning of ${\lvert {X} \rvert }$ is the least strict upper bound on elements of X. There is one exception to the number sort and set sort notation: The name of an arbitrary bounded field will be denoted F despite bounded fields being objects of the number sort. Note that only in the language of $V^0_2$ we have two sorts (i.e., the number sort and the set sort), and we use the uppercase and lowercase letters to distinguish between them. However, in the language of $\mathrm {PV}$ , there is only one sort, i.e., the number sort. Therefore, when we are working in a theory in the language of $\mathrm {PV}$ , such as $\mathrm {PV}_1$ or $S^1_2$ , we freely use uppercase letters also to denote objects of the number sort.

A $\Sigma ^B_0$ -formula is a bounded formula in this new language without quantification of the set sort. Following [Reference Jeřábek13], the theory $V^0_2$ can be axiomatized by $T_2$ , the basic axioms

$$ \begin{align*} &{\lvert {X} \rvert}\neq 0 \to (\exists x)(x\in X \land {\lvert {X} \rvert}=x+1)\\ &x\in X \to x < {\lvert {X} \rvert}\\ &(\forall x)((x\in X \leftrightarrow x\in Y) \to X=Y) \end{align*} $$

and the comprehension schema for $\Sigma ^B_0$ -formulas. That is, for every $\Sigma ^B_0$ -formula $\varphi $ , the following is an axiom schema,

(φ−COMP) $$ \begin{align}(\exists X\leq x)(\forall u < x)(u \in X \leftrightarrow \varphi(u)) \end{align} $$

where a bounded quantification of an element of the set sort $(\exists Y \leq t)(\dots )$ is interpreted as $(\exists Y)( {\lvert {Y} \rvert }\leq t \land \dots )$ .

Note that using sets, we can encode sequences of the elements of the number sort, $X^{(i)}$ being the i-th element of such encoding, where X is an element of the set sort and i an element of the number sort. We obtain the theory $\text {VTC}^0_2$ by extending $V^0_2$ by the axiom $(\mathrm {CARD})$ :

$$ \begin{align*} (\forall n)(\forall X)(\exists Y)(&Y^{(0)}=0 \land \\&(\forall i<n )((i\not \in X \to Y^{(i+1)}=Y^{(i)}) \land\\&\:\phantom{(\forall i<n)}\: (i\in X \to Y^{(i+1)} = Y^{(i)}+1))) \end{align*} $$

In essence, the theory $\text {VTC}^0_2$ is a simple extension of the two-sorted theory $\text {VTC}^0$ originally defined in [Reference Cook and Nguyen6] by the smash function $\#$ for the number sort, and in our setting also by all $\mathrm {PV}$ -symbols for the number sort. In this work, we understand the theory $\text {VTC}^0$ as a theory whose axioms are the ones of $\text {VTC}^0_2$ which do not contain the symbol for the smash function $\#$ .

We say a formula in the language of $\text {VTC}^0_2$ is $\Sigma ^B_1$ if it is equivalent over predicate calculus to a formula that contains only bounded number sort quantifications, bounded existential set sort quantification and no negations appear before any of the existential set sort quantifications. A function is $\Sigma ^B_1$ -definable in $\text {VTC}^0_2$ if its graph can be defined in the standard model using a $\Sigma ^B_1$ -formula $\varphi (X,Y)$ such that $\text {VTC}^0_2 \vdash (\forall X)(\exists ! Y)\varphi (X,Y)$ . It can be shown [Reference Cook and Nguyen6, Theorem IX.3.7.] that $\text {VTC}^0_2$ proves the comprehension axiom which we shall denote $\Sigma ^B_0(\text {card})\text {-}\mathrm {COMP}$ . This comprehension axiom allows the $\Sigma ^B_0$ -formulas to contain new function symbols each computing a $\Sigma ^B_1$ -definable function in $\text {VTC}^0_2$ , similarly it proves the induction axiom $\Sigma ^B_0(\text {card})\text {-}\mathrm {IND}$ , which allows such formulas in the induction axiom.

2.2 Algebraic primitives in bounded arithmetic

Let us start with the formalization of elementary number theory and polynomial arithmetic in $\mathrm {PV}_1$ . For numbers x, y we denote x divides y by $x \mid y$ . There is a well-behaved $\mathrm {PV}$ -symbol $x\ \mathrm { mod }\ m$ which computes the remainder of x modulo m. The primality of a number x is defined by the $\Pi ^b_1$ -formula $\text {Prime}(x)$ :

$$\begin{align*}x>1 \land (\forall y\leq x)(y \mid x \to (y=1 \lor y=x)).\end{align*}$$

Coding of both sets and sequences of elements can be developed in $\mathrm {PV}_1$ , here we will describe the main ideas. We use the notation $1^{(r)}$ to denote the number whose binary expansion consists of r-many ones, in other words, the number r is of logarithmic size. Coding of sets is simple, there is a well-behaved $\mathrm {PV}$ -symbol $\textrm {bit}(x,i)$ which outputs the i-th bit of the number x, the elementhood relation $i\in x$ is then defined to be equivalent to $\textrm {bit}(x,i)=1$ . Regarding sequences, a sequence $( a_1,\dots , a_k),$ where $1^{(k)}$ exists, can be coded by a pair $\langle a,b \rangle $ , with a consisting of a number whose binary expansion is the concatenation of the binary expansions of $a_1, a_2, \dots , a_k$ and b is the number whose binary expansion contains $1$ at the positions which correspond to the beginning of each $a_i$ . We shall denote the pair $\langle a,b\rangle $ by $\langle a_1,\dots ,a_k\rangle $ . More details on coding of sequences in $\mathrm {PV}_1$ can be found in [Reference Krajíček15, Section 5.4]. Sums and products over sequences can also be defined by the obvious iterative algorithm. Such an algorithm obtains a sequence of numbers and outputs the iterated sum/product as a single number.

Let us note that sometimes we consider sets which are not neccesarily codeable in $\mathrm {PV}_1$ but are definable by a formula: These are just abbreviations in the meta-language where we talk about a definable predicate as if it were the set of all elements which satisfy it. As such, definable sets are not quantifiable. Of special importance are sets of the form $\{x;C(x)=1\}$ for a Boolean circuit C, as these can appear in the induction formulas. We always make it clear when a set is codeable as oppose to definable.

Polynomials are defined to be sequences of coefficients such that the number of coefficients is one more than the degree of the polynomial, with the addition, multiplication and composition defined as usual, division defined using the long division algorithm, and exponentiation modulo some other polynomial defined using exponentiation by squaring. Divisibility of polynomials is defined as usual, the notation $f\mid g$ meaning that the polynomial f divides g. A polynomial is called irreducible if it cannot be written as a product of two polynomials, both having positive degrees. We will sometimes call polynomials formalized like this low degree polynomials, as their degree is bounded by a number of logarithmic size. Later in this section we will define a second formalization of polynomials in a two sorted theory, and we will call polynomials following this second formalism high degree polynomials.

The basic properties of the greatest common divisor ( $\gcd $ ) of numbers are essential for many arguments. The following is well-known (see [Reference Jeřábek12]):

Lemma 2.1 ( $\mathrm {PV}_1$ , Euclid’s algorithm)

There is a $\mathrm {PV}$ -function symbol $\gcd $ such that $\mathrm {PV}_1$ proves

$$ \begin{align*} &\gcd(x,y) \mid x\\ &\gcd(x,y) \mid y\\ &(z \mid x \land z \mid y) \to (z \mid \gcd(x,y)), \end{align*} $$

and also a $\mathrm {PV}$ -function symbol $\text {xgcd}$ for which $\mathrm {PV}_1$ proves

$$ \begin{align*} (\text{xgcd}(x,y) = (g,u,v)) \to (g=\gcd(x,y) \land g=ux+vy). \end{align*} $$

Throughout this work, we introduce $\mathrm {PV}$ -symbols by declaring their name and properties inside the Lemma environment. Therefore, in the subsequent parts of this work, $\gcd $ and $\text {xgcd}$ in any extension of $\mathrm {PV}_1$ denote specific $\mathrm {PV}$ -symbols which satisfy the statement of the Lemma 2.1. We are now ready to define the first algebraic axiom we need for our formalization. Throughout the paper, we will use calligraphic uppercase letters ${\mathcal {X}}$ , $\mathcal {Y}$ , $\dots $ for formal variables of polynomials.

Definition 2.2 (Generalized Fermat’s Little Theorem)

Let $\text {GFLT}$ be the natural $\Sigma ^b_1$ -sentence formalizing the following statement, where the exponentiation of polynomials is given by a $\mathrm {PV}$ -symbol for exponentiation by repeatedly squaring modulo the polynomial ${\mathcal {X}}^r-1$ .

The validity of $\text {GFLT}$ follows in a sufficiently strong meta-theory by applying binomial theorem to the expresison $({\mathcal {X}}+a)^p$ and considering which coefficients are divisible by p, this gives us $({\mathcal {X}}+a)^p \equiv {\mathcal {X}}^p + a \ (\mathrm{mod }\ {p})$ which we take modulo ${\mathcal {X}}^r-1$ . Since there are exponentially many monomials in the expansion of $({\mathcal {X}}+a)^p$ , it is not clear how to adapt the proof strategy in $\mathrm {PV}_1$ even if we assume the ordinary Fermat’s Little Theorem as an axiom.

Let us now discuss the formalization of algebraic concepts in $\text {VTC}^0_2$ . As an extension of $T_2$ , all function and relational symbols on the number sort are carried over from $\mathrm {PV}_1$ . More interesting is the case of arithmetical operations over the set sort, where we interpret the set X as a number $\sum _{u\in X}2^u$ . Already $V^0_2$ can prove the totality and basic properties of addition and ordering. However, multiplication is $\text {TC}^0$ -complete. Thus, it is known that $V^0_2$ cannot prove it is total as this would contradict known lower bounds against $\text {AC}^0$ . Coding of sequences of elements of the set sort can be developed in $\text {VTC}^0_2$ , with i-th element of a sequence S being $S^{[i]}$ . It is also well-known that $\text {VTC}^0_2$ can prove the totality and basic properties of multiplication. Moreover, $\text {VTC}^0_2$ can $\Sigma ^B_1$ -define iterated addition $\sum _{i<n}X^{[i]}$ and prove

$$ \begin{align*} \sum_{i<0} X^{[i]} &= 0,\\ \sum_{i<n+1} X^{[i+1]} &= X^{[n]}+\sum_{i<n} X^{[i]}. \end{align*} $$

Only recently has Jeřábek [Reference Jeřábek13] shown that $\text {VTC}^0_2$ can also $\Sigma ^B_1$ -define iterated multiplication and prove the analogous recursive properties. This also implies that it can define the division of integers.

Theorem 2.3 [Reference Jeřábek13]

$\text {VTC}^0$ can $\Sigma ^B_1$ -define iterated products $\prod _{i<n} X^{[i]}$ and prove the iterated multiplication axiom $\text {IMUL}$ :

$$ \begin{align*} \prod_{i<0} X^{[i]} &= 1,\\ \prod_{i<n+1} X^{[i+1]} &= X^{[n]}\cdot\prod_{i<n} X^{[i]}. \end{align*} $$

Moreover, $\text {VTC}^0$ can $\Sigma ^B_1$ -define a function $\left \lfloor {X/Y} \right \rfloor $ such that it proves

$$\begin{align*}Y\neq 0 \to \left \lfloor {X/Y} \right\rfloor\cdot Y \leq X < (\left \lfloor {X/Y} \right\rfloor+1)\cdot Y.\end{align*}$$

Finally, let us treat polynomials encoded by elements of the set sort as a sequence of coefficients, where each coefficient is an element in the number sort, which we shall call high degree polynomials. The totality of addition of high-degree polynomials is straightforward, and using iterated addition, the totality of their multiplication can be proved in $\text {VTC}^0$ . We will observe in Theorem 6.11 that the Kung-Sieveking $\text {TC}^0$ -algorithm as presented in [Reference Healy and Viola9] for the division of polynomials can also be proved correct in $\text {VTC}^0_2$ which also implies the totality of division for high degree polynomials.

3.1 Proof of the correctness

We begin by providing a high-level overview of the proof of correctness of the AKS algorithm (Algorithm 1) [Reference Agrawal, Kayal and Saxena1], here $\text {ord}_r(n)$ is the multiplicative order of n modulo r and $\text {log}\,$ is the base $2$ logarithm. In doing so, we restate and give new alphabetical names to key Lemmas and Theorems of [Reference Agrawal, Kayal and Saxena1] to avoid confusion with the numbering in our work. The key number-theoretic statement behind the algorithm is the following:

Lemma (A) [Reference Agrawal, Kayal and Saxena1, Lemma 2.1]

Let $a\in \mathbb {Z}$ , $n\in \mathbb {N}$ , $n\geq 2$ and $\gcd (a,n)=1$ . Then n is prime if and only if

$$\begin{align*}({\mathcal{X}}+a)^n\equiv {\mathcal{X}}^n+a \ (\mathrm{mod }\ {n}).\end{align*}$$

The AKS algorithm essentially emerges as an effectivization of this characterization of primality. As testing for this equality explicitly requires comparing objects of size exponential in ${\lvert {n} \rvert }$ , the AKS algorithm instead checks the equality modulo a low degree polynomial ${\mathcal {X}}^r-1$ for polynomially many values of a. Since the statement of this lemma cannot even be expressed in the language of $\mathrm {PV}$ , in the formalization, we instead supplement it by the $\text {GFLT}$ axiom. This axiom is what remains of Lemma A by keeping the only if direction and taking the equality mod ${\mathcal {X}}^r-1$ for r polynomial in ${\lvert {n} \rvert }$ .

This axiom implies the following direction of the correctness.

Next, the goal is to prove that the number r, which is essentially found by brute force in the AKS algorithm, always exists and has size polynomial in ${\lvert {n} \rvert }$ . This is Lemma D, which is, in turn, proved using Lemma C. Here, we use the symbol $\text {lcm}$ to denote the function computing the least common multiple.

Lemma (C) [Reference Agrawal, Kayal and Saxena1, Lemma 3.1]

Let $\text {LCM}(m)$ denote the $\text {lcm}$ of the first m numbers. Then for $m\geq 7$ :

$$\begin{align*}\text{LCM}(m)\geq 2^m.\end{align*}$$

We use slightly different bounds in our formalization, but they are always polynomially related to the original ones.

From now on, we assume that on the input n the AKS algorithm answered PRIME. We take r from the statement of Lemma D and fix some prime $p \mid n$ such that $\text {ord}_r(p)> 1$ , the rest of the proof consists of showing that $n=p$ . Furthermore, we fix the number $\ell = \left \lfloor {\sqrt {\phi (r)}} \right \rfloor \cdot \left \lfloor {\text {log}\, n} \right \rfloor $ .

The proof then continues by defining the concept of introspectivity.

Definition [Reference Agrawal, Kayal and Saxena1, Definition 4.4]

For a polynomial $f({\mathcal {X}})$ and a number $m\in \mathbb {N}$ , we say that m is introspective for $f({\mathcal {X}})$ if

$$\begin{align*}[f({\mathcal{X}})]^m \equiv [f({\mathcal{X}}^m)] \ (\mathrm{mod }\ {{\mathcal{X}}^r-1}).\end{align*}$$

Together Lemma A and our assumptions about n and p imply that $\frac {n}{p}$ and p are both introspective for all $({\mathcal {X}}+a)$ , $0\leq a \leq \ell $ . Lemma F then allows us to show that for the sets $I=\{(\frac {n}{p})^i p^j; i,j \geq 0\}$ and $P = \{\prod _{a}({\mathcal {X}}+a)^{e_a};e_a\geq 0\}$ it holds that every number from I is introspective for every polynomial in P.

Now we finally define $G = I\ \mathrm{ mod }\ r$ and $\mathcal {G} = P \ \mathrm{ mod }\ h$ , where h is an irreducible factor of the cyclotomic polynomial $Q_r$ over the field $\mathbb {F}_p$ . After setting $t={\lvert {G} \rvert }$ , we can state the last two technical Lemmas.

Since the AKS algorithm checks whether n is a perfect power and we assume that it is not (otherwise, the algorithm outputs COMPOSITE), we get that both bounds on $\mathcal {G}$ hold. By showing they are incompatible we obtain:

Putting Lemma B and Lemma H together, we get:

3.2 Overview of our formalization

Let us start with the formalization of the AKS algorithm as a $\mathrm {PV}$ -symbol. The algorithm begins by checking whether the number on the input is not a perfect power; this can be checked in polynomial time, and the algorithm as a $\mathrm {PV}$ -symbol can be proved correct in $\mathrm {PV}_1$ .

Lemma 3.1. There is a $\mathrm {PV}$ -symbol for which $\mathrm {PV}_1$ proves:

Next, one has to fix some upper bound for the number r, which is polynomial in ${\lvert {n} \rvert }$ . We will later prove in $S^1_2$ that such a bound exists. For convenience, let us also assume that the algorithm actually checks for the slightly stronger $\text {ord}_r(n)> {\lvert {n} \rvert }^2$ . We show this stronger assumption is justified in Lemma 5.19 by the same argument as in [Reference Agrawal, Kayal and Saxena1]. For any natural number r, the function $\phi (r)$ is Euler’s totient function which outputs the number of numbers less than r that are relatively prime to r. The value $\phi (r)$ can be computed by a $\mathrm {PV}$ -symbol which obtains $1^{(r)}$ on the input (see Lemma 4.5). The function $\lfloor {\sqrt {x}} \rfloor $ can be computed by a binary search for the value y which satisfies $y^2 \leq x < (y+1)^2$ . The function $\lfloor {\text {log}\, x} \rfloor $ is exactly equal to ${\lvert {x} \rvert }-1$ . All of these algorithms can be straightforwardly formalized as $\mathrm {PV}$ -symbols. Altogether, the AKS algorithm can be formalized as a $\mathrm {PV}$ -symbol , which outputs $1$ if and only if the algorithm would output PRIME. By the correctness of the AKS algorithm, we mean the sentence :

We prove the correctness by following the outline of the proof as in the previous section. For each Lemma or Theorem used in the formalization, we always strive to use the weakest possible theory for the given argument.

In Section 4, we show that $S^1_2$ proves the existence of cyclotomic extensions of finite fields. This is important later in the argument to prove the existence of the polynomial h.

For the formalization, we will use the following congruence property. Recall that we fixed the number r from Lemma D satisfying $r \leq \text {max} \{3, \lceil \text {log}\,^5 n \rceil \}$ and $\text {ord}_r(n)> \left \lfloor {\text {log}\,{n}} \right \rfloor ^2$ . We also fixed $\ell = \left \lfloor {\sqrt {\phi (r)}} \right \rfloor \cdot \left \lfloor {\text {log}\, n} \right \rfloor $ .

Lemma (Congruence)

Let n be a number such that holds, i.e., the AKS algorithm asserts that n is prime, and let r be the value provided by the algorithm satisfying $\text {ord}_r(n)> |n|^{2}$ . Assume p is a prime divisor of n such that $\text {ord}_r(p)>1$ . And let us fix $\ell = \left \lfloor {\sqrt {\phi (r)}} \right \rfloor \cdot \left \lfloor {\text {log}\, n} \right \rfloor $ . In $S^1_2+\text {GFLT}$ it holds that for every $0 \leq a \leq \ell $

$$\begin{align*}({\mathcal{X}}+a)^{\frac{n}{p}} \equiv {\mathcal{X}}^{\frac{n}{p}}+a \ (\mathrm{mod }\ {{\mathcal{X}}^r-1, p}). \end{align*}$$

We provide most of our formalization of the original proof in Section 5 in the theory $S^1_2 + \mathrm {iWPHP} + \mathrm {RUB} + \text {GFLT}$ . We start in Section 5.1 by proving Legendre’s formula in $\mathrm {PV}_1$ ; we use it in Section 5.2 to prove our version of Lemma C, which is used in Section 5.3 to prove Lemma D. In Section 5.4, we prove the Congruence Lemma and in Section 5.5, we formalize the concept of introspectivity and prove Lemma E.

Since the property of a polynomial being in the group $\mathcal {G}$ is not easily formulated by a $\mathrm {PV}$ -predicate, we instead use the predicate $\hat P$ recognizing all those polynomials over F with degree at most r. Our version of Lemma F instead of an inequality states that there exists a function $\tau $ from $\{1,\dots , \binom {t+\ell }{t-1}\}$ into $\hat P$ , which satisfies . To prove Lemma F in Section 5.6, we first formalize the Combinatorial Number System, which assigns to each number $i\leq \binom {m}{k}$ a unique k-element subset of $\{1,\dots ,m\}$ , when m is given in unary. Our version of Lemma G, which again replaces inequality by an existence of a function $g:\hat P \to n^{\lfloor {\sqrt {t}} \rfloor }$ , with the property , is proved in Section 5.7 using the axiom $\mathrm {RUB}$ . We finish in Section 5.8 by proving Lemma H: the composition of the functions from Lemmas F and G results in an injective function which is in contradiction with the axiom $\mathrm {iWPHP}$ .

The remainder of the formalization is done in Section 6, where we prove that $\text {VTC}^0_2$ proves the consequences of $S^1_2+\mathrm {iWPHP}+\mathrm {RUB}+\text {GFLT}$ . We thus obtain that both $\text {VTC}^0_2$ and $T^{\text {count}}_2$ prove .

4.1 Formalization of algebraic structures

In this section, we shall prove in $\mathrm {PV}_1$ that over the finite fields $\mathbb {Z}/p$ , where p is prime, there are r-th cyclotomic polynomials for arbitrary $r<p$ represented in unary. We also define a concept of bounded fields and use $S^1_2+\text {GFLT}$ to prove that the r-th cyclotomic extension of $\mathbb {Z}/p$ exists. Bounded fields are simply finite fields on a domain $[b]=\{0,\dots , b-1\}$ for some number b, such that their operations are computed by boolean circuits. An analogous definition was already provided by Jeřábek in [Reference Jeřábek11]; here, we make the possibility of the field operation being coded by a circuit an explicit part of the definition to allow quantification over bounded fields.

Definition 4.1 ( $\mathrm {PV}_1$ )

A bounded field is a tuple $(b,\tilde 0, \tilde 1,C_i,C_o,C_a,C_m)$ of elements, where $C_i$ is a circuit computing $i:[b]\to [b]$ , $C_o$ is a circuit computing $o:[b]\setminus \{\tilde 0\} \to [b]\setminus \{\tilde 0\}$ , $C_a$ is a circuit computing $a:[b]^2\to [b]$ and $C_m$ is a circuit computing $m:[b]^2\to [b]$ such that a as addition, m as multiplication, i as additive inverse and o as multiplicative inverse satisfy the field axioms on the universe $[b]$ with $\tilde 1$ as the $1$ element, and $\tilde 0$ as the $0$ element. That is, for all $x,y,z \in [b]$ we have

(associativity of a) $$\begin{align}a(x,a(y,z))&= a(a(x,y),z) \end{align} $$

(associativity of m) $$\begin{align} m(x,m(y,z))&= m(m(x,y),z) \end{align} $$

(commutativity of a) $$\begin{align} a(x,y)&=a(y,x) \end{align} $$

(commutativity of m) $$\begin{align} m(y,x)&=m(y,x) \end{align} $$

(neutrality of 0) $$ \begin{align} a(x,\tilde 0) &= x \end{align} $$

(neutrality of 1) $$ \begin{align} m(x, \tilde 1) &= x \end{align} $$

(i is the additive inverse) $$\begin{align}a(x, i(x)) &= \tilde 0 \end{align} $$

(distributivity) $$ \begin{align} m(a(x,y),z) &= a(m(x,z),m(y,z)), \end{align} $$

and for all nonzero $x\in [b]:$

(o is the multiplicative inverse) $$\begin{align}m(x,o(x))=\tilde 1. \end{align} $$

When a bounded ring/field is understood from the context, we shall denote $a(x,y)$ as $x+y$ , $m(x,y)$ as $x\cdot y$ , $o(x)$ as $x^{-1}$ , $i(x)$ as $-x$ , $\tilde 1$ as $1$ , and $\tilde 0$ as $0$ .

In sections 4 and 5, the usual name for a bounded field is F. Low degree polynomials over a bounded field F are defined as usual in $\mathrm {PV}_1$ , that is as sequences of elements of F of length equal to the degree of the polynomial plus one, and do not require special treatment. That is, for each bounded field F there is a $\mathrm {PV}$ -symbol which naturally encodes a predicate $f\in F[{\mathcal {X}}]$ , we will therefore freely use this notation.

The following is straightforward, as the correctness of the Euclid’s algorithm for polynomials can be proved analogously to the variant for integers.

Lemma 4.3 ( $\mathrm {PV}_1$ , Euclid’s algorithm)

Let F be a bounded field, then there are $\mathrm {PV}$ -symbols $\gcd $ and $\text {xgcd}$ such that for any $f,g\in F[{\mathcal {X}}]$ we have

$$ \begin{align*} \gcd(f,g) &\in F[{\mathcal{X}}]\\ \text{xgcd}(f,g)&=(h,u,v)\\ h,u,v&\in F[{\mathcal{X}}]\\ h&=\gcd(f,g)\\ h&=uf+vg, \end{align*} $$

and

$$ \begin{align*} \gcd(f,g) & \mid f\\ \gcd(f,g) & \mid g\\ (\forall t\in F[{\mathcal{X}}])((t\mid f \land t & \mid g) \to t \mid \gcd(f,g)). \end{align*} $$

Moreover, $\gcd (f,g)$ is monic, that is the coefficient of the highest degree monomial is $1$ .

4.2 Existence of Cyclotomic extensions

We will start by proving basic properties of the Euler’s totient function $\phi $ , which is definable in $\mathrm {PV}_1$ for numbers represented in unary.

Lemma 4.5 ( $\mathrm {PV}_1$ )

There is a $\mathrm {PV}$ -symbol , such that $\mathrm {PV}_1$ -proves

we will simply denote the value as $\phi (r)$ .

Proof. We start with the observation that $\{1,\dots ,r\} = \bigcup _{d\mid r} S_d^r$ . By taking the cardinality of both sides, we get

(†) $$ \begin{align} r &= \sum_{d\mid r} {\lvert {S^r_d} \rvert} \nonumber\\ &= \sum_{d \mid r} \phi(r/d) \end{align} $$

(‡) $$ \begin{align} &= \sum_{d\mid r} \phi(d),\end{align} $$

where ( $\dagger $ ) follows from Lemma 4.8 and ( $\ddagger $ ) follows from the fact that the map $d\mapsto r/d$ is an involution on the set of all divisors of r.

We will now prove basic properties of polynomials over bounded fields which are needed to prove the existence of cyclotomic polynomials.

Proof. Assume that $l = km$ . Then we have

$$ \begin{align*} ({\mathcal{X}}^k-1) (\sum_{i=1}^m {\mathcal{X}}^{(m-i)k}) &= (\sum_{i=1}^m {\mathcal{X}}^{(m-i)k+k}) - (\sum_{i=1}^m {\mathcal{X}}^{(m-i)k})\\ &= (\sum_{i=1}^m{\mathcal{X}}^{(m-i+1)k})-(\sum_{i=1}^m {\mathcal{X}}^{(m-i)k})\\ &= {\mathcal{X}}^l +(\sum_{i=2}^{m}{\mathcal{X}}^{(m-i+1)k})-(\sum_{i=1}^{m-1} {\mathcal{X}}^{(m-i)k})-1\\ &= {\mathcal{X}}^l +(\sum_{i=1}^{m-1}{\mathcal{X}}^{(m-i-1+1)k})-(\sum_{i=1}^{m-1} {\mathcal{X}}^{(m-i)k})-1\\ &= {\mathcal{X}}^l - 1.\\[-38pt] \end{align*} $$

Proof. bounded Assume that

$$ \begin{align*} \text{xgcd}(g,h) &= (1,u,v)\\ \text{xgcd}(f,h) &=(g_1,u_1,v_1)\\ \text{xgcd}(fg,h)&=(g_2,u_2,v_2), \end{align*} $$

we will show that $g_1=g_2$ . To prove that $g_2 \mid g_1$ , we will multiply the equality $ug+vh=1$ by $g_1$ to obtain

$$ \begin{align*} (ug+vh)g_1&=g_1\\ (ug+vh)(u_1f+v_1h)&=g_1\\ ugu_1f + ugv_1h+vhu_1f+ vv_1h^2&=g_1\\ fg(uu_1)+h(ugv_1+vu_1f+vv_1h)&=g_1, \end{align*} $$

and since $g_2$ is a common divisor of both $fg$ and h, it is a divisor of $g_1$ . Analogously, by multiplying the equality $ug+vh=1$ by $g_2$ we obtain

$$ \begin{align*} (ug+vh)g_2&=g_2\\ (ug+vh)(u_2fg+v_2h)&=g_2\\ ug^2u_2f + ugv_2h+vhu_2fg+ vv_2h^2&=g_2\\ f(ug^2u_2)+h(ugv_2+vu_2fg+vv_2h)&=g_2, \end{align*} $$

and $g_1$ is a common divisor of both f and h, therefore a divisor of $g_2$ .

Lemma 4.12 ( $\mathrm {PV}_1$ )

Let $1^{(k)}$ and $1^{(l)}$ be numbers, $k,l\geq 1$ , then

$$\begin{align*}\gcd({\mathcal{X}}^k-1,{\mathcal{X}}^l-1)={\mathcal{X}}^{\gcd(k,l)}-1,\end{align*}$$

over any bounded field.

Proof. By induction on $\text {max}\{k,l\}$ . If $\text {max}\{k,l\}=1$ , the equality is trivial.

Assume that the statement holds for all instances where $\text {max}\{k,l\}<s$ for some s, where $1^{(s)}$ exist, we will prove it for the case $\text {max}\{k,l\}=s$ . Without loss of generality, we can assume $k<l$ , as the case $k=l$ is trivial. Note that this is an instance of the second mathematical induction for open formulas and it is available in $\mathrm {PV}_1$ because the number $\text {max}\{k,l\}$ is a length as the corresponding quantifier in the induction formula is sharply bounded.

Let $r,q$ be numbers such that $l=qk+r$ , and $r<k$ , by Lemma 4.10 there is a polynomial f, such that $f\cdot ({\mathcal {X}}^k-1)=({\mathcal {X}}^{kq}-1)$ . We have

$$ \begin{align*} {\mathcal{X}}^l-1 &= {\mathcal{X}}^{kq+r}-1\\ &= {\mathcal{X}}^r({\mathcal{X}}^{kq}-1)+{\mathcal{X}}^r-1\\ &= {\mathcal{X}}^r\cdot f \cdot ({\mathcal{X}}^k-1) + {\mathcal{X}}^r-1, \end{align*} $$

and thus by Lemma 4.11

$$\begin{align*}\gcd({\mathcal{X}}^k-1,{\mathcal{X}}^l-1)=\gcd({\mathcal{X}}^k-1,{\mathcal{X}}^r-1)={\mathcal{X}}^{\gcd(k,r)}-1={\mathcal{X}}^{\gcd(k,l)}-1.\\[-39pt] \end{align*}$$

Proof. By induction on k. The case where $k=1$ is trivial. Assume the lemma holds for $k-1$ , then

(†) $$ \begin{align} \gcd(g,\prod_{i=1}^kf_i) &= \gcd(g,f_k \prod_{i=1}^{k-1}f_i) \nonumber\\ &=\gcd(g,\prod_{i=1}^{k-1}f_i) \end{align} $$

(‡) $$ \begin{align} &=1, \end{align} $$

where ( $\dagger $ ) follows from the previous line by Lemma 4.11 and ( $\ddagger $ ) follows from the induction hypothesis.

Proof. By induction on k. For $k=1$ the statement is trivial.

Assume that the statement holds for $k-1$ , and that we want to prove it for the sequence $\langle f_1,\dots ,f_k\rangle $ and $g\in F[{\mathcal {X}}]$ satisfying for every $1\leq i \leq k: f_i\mid g$ and also that for $i\neq j$ we have $\gcd (f_i,f_j)=1$ . Then for $h=\prod _{i=1}^{k-1} f_i$ we have $h\mid g$ and by Lemma 4.13 also $\gcd (h,f_k)=1$ . Assume that $\text {xgcd}(h,f_k) = (1,u,v)$ , therefore $uh+vf_k=1$ and fix polynomials $s,t\in F[{\mathcal {X}}]$ satisfying $sh = g$ and $tf_k = g$ .

Then we have

$$ \begin{align*} uh+vf_k&=1\\ uhg+vf_kg&=g\\ uhtf_k + vf_ksh &= g\\ hf_k(ut+vs)&=g, \end{align*} $$

and thus $\prod _{i=1}^kf_k = hf_k \mid g$ .

Lemma 4.16 ( $\mathrm {PV}_1$ )

Let F be a bounded field. If $f,g\in F[{\mathcal {X}}]$ , then

$$ \begin{align*} (f+g)'&=f'+g'\\ (fg)'&=f'g+fg'. \end{align*} $$

We are now ready to prove the existence of cyclotomic polynomials in $\mathrm {PV}_1$ , the proof we use differs from the standard proof by only using elementary concepts and thus not needing the definition of cyclotomic polynomials which uses the field of complex numbers.

Theorem 4.18 ( $\mathrm {PV}_1$ )

There is a $\mathrm {PV}$ -symbol such that $\mathrm {PV}_1$ proves that for every prime p, and every number $1^{(r)}$ , $1\leq r < p$ , we have that is a degree $\phi (r)$ polynomial over $\mathbb {Z}/p$ , such that

$$ \begin{align*} &Q_r \mid {\mathcal{X}}^r-1,\\ \forall r'\in\{1,\dots,r-1\}:&\gcd (Q_r, X^{r'}-1)=1. \end{align*} $$

Proof. Let us first define to be either ${\mathcal {X}}-1$ in the case that $r=1$ and otherwise , possibly discarding the remainder. In the rest of this proof, we will denote the value of by $Q_{a}$ . We will later show that the product $\prod _{d\mid r, d<r} Q_d$ indeed divides ${\mathcal {X}}^r-1$ .

The proof continues by induction on the sharply bounded formula $\psi (r)$ which is formed as a conjunction of the following formulas:

• • $(\forall r' \leq {\lvert {1^{(r)}} \rvert })(r'\geq 1 \to ({\mathcal {X}}^{r'}-1 = \prod _{d\mid r'} Q_d))$

• • $(\forall r' \leq {\lvert {1^{(r)}} \rvert })(r'\geq 1 \to (\deg Q_{r'} = \phi (r')))$

• • $(\forall r_1, r_2 \leq {\lvert {1^{(r)}} \rvert })((r_1 \neq r_2 \land r_1 \geq 1 \land r_2 \geq 1) \to \gcd (Q_{r_1},Q_{r_2})=1).$

The formula $\psi (r)$ is valid when $r=1$ , as $Q_1={\mathcal {X}}-1$ , and the third conjunct of $\psi (1)$ is vacuously true.

Now for the induction step assume that $\psi (r-1)$ is true. We will use it to prove $\psi (r)$ . For distinct divisors $d_1,d_2$ of r which are not equal to r we have that $\gcd (Q_{d_1},Q_{d_2})=1$ and by Lemma 4.10 every $d\mid r, d<r$ satisfies $Q_{d} \mid {\mathcal {X}}^{d}-1 \mid {\mathcal {X}}^r-1$ , we can obtain by Lemma 4.14 that $\prod _{d\mid r, d<r} Q_d \mid {\mathcal {X}}^r-1$ .

Regarding the second conjunct, the induction hypothesis implies that

$$\begin{align*}\deg \prod_{d\mid r, d<r} Q_d = \sum_{d\mid r, d<r}\phi(r),\end{align*}$$

by the definition of $Q_r$ , we have that $\deg Q_r = r-\sum _{d\mid r, d<r}\phi (r)$ which is equal to $\phi (r)$ by Lemma 4.9.

To finish the induction step it remains to show that $\gcd (Q_r, Q_{r'})=1$ for every $1 \leq r' < r$ . Assume that $g = \gcd (Q_r,Q_{r'})$ , then

(†) $$ \begin{align} g \mid Q_r & = \frac{{\mathcal{X}}^r-1}{\prod_{d\mid r, d<r} Q_d} \end{align} $$

Let $r" = \gcd (r,r')$ , by Lemma 4.12 and the properties of $\gcd $ we have

$$\begin{align*}g=\gcd(Q_r,Q_{r'}) \mid \gcd({\mathcal{X}}^{r}-1,{\mathcal{X}}^{r'}-1) = {\mathcal{X}}^{\gcd(r,r')}-1=\prod_{d\mid r"}Q_d,\end{align*}$$

thus $g \mid \prod _{d\mid r"} Q_d \mid \prod _{d\mid r, d<r} Q_d$ , combining this with ( $\dagger $ ) gives $g^2 \mid {\mathcal {X}}^r-1$ . This implies by Lemma 4.17 that $\deg g =0$ , as $r<p$ gives us $\gcd ({\mathcal {X}}^r-1,r{\mathcal {X}}^{r-1})=1$ . This concludes the induction step.

To obtain the statement of the theorem, it remains to prove the equality $\gcd (Q_r,{\mathcal {X}}^{r'}-1)=1$ for any $0<r'<r$ . By the third conjunct of $\psi (r)$ and Lemma 4.13 we have

$$\begin{align*}\gcd(Q_r,{\mathcal{X}}^{r'}-1)=\gcd(Q_r,\prod_{d\mid r'} Q_d)=1.\\[-42pt]\end{align*}$$

To prove the existence of the polynomial h from the proof of the correctness in [Reference Agrawal, Kayal and Saxena1], we will first prove some basic properties of exponentiation by squaring.

Proof. We will proceed by open polynomial induction on m. If $m=1$ , the statement is trivial.

For the induction step, we will assume the statement for $\left \lfloor {m/2} \right \rfloor $ . The case where there is l such that $m-1=2l$ is trivial, as by the definition of exponentiation by squaring we have

$$\begin{align*}f^m \equiv (f^{l})^2 f \equiv f^{m-1} \cdot f \ (\mathrm{mod }\ {g,p}).\end{align*}$$

In the case where there is l such that $m=2l$ , then we have by definition of exponentiation by squaring

$$ \begin{align*} f^m&\equiv (f^l)^2 \ (\mathrm{mod }\ {g,p})\\ f^{m-1} &\equiv (f^{l-1})^2 \cdot f\ (\mathrm{mod }\ {g,p}), \end{align*} $$

which implies

(†) $$ \begin{align} f^{m-1}f &\equiv (f^{l-1})^2 \cdot f^2 \nonumber\\ &\equiv (f^{l-1} f)^2 \nonumber\\ &\equiv (f^l)^2 \\ &\equiv f^m \ (\mathrm{mod }\ {g,p}),\nonumber \end{align} $$

where $(\dagger )$ follows from the induction hypothesis. The second congruence can be proved analogously.

Lemma 4.21 ( $\mathrm {PV}_1$ , Divisor lemma)

Let p be a prime, l be a number and let f, g and $g_0$ be polynomials. If $g_0\mid g$ , then

$$\begin{align*}[f]_g^l \equiv [f]_{g_0}^l \ (\mathrm{mod }\ {g_0,p}),\end{align*}$$

where $[f]_g^l$ and $[f]^l_{g_0}$ denote exponentiation by squaring modulo g and $g_0$ respectively.

Proof. By induction on l, if $l=0$ the statement is trivial.

For the induction step, assume the statement holds for l. Then by Lemma 4.20 we have

$$\begin{align*}[f]^{l+1}_g \equiv [f]^{l}_g\cdot f \ (\mathrm{mod }\ {g,p}),\end{align*}$$

since $g_0\mid g$ , then also

(*) $$ \begin{align} [f]^{l+1}_g &\equiv [f]^{l}_g\cdot f \ (\mathrm{mod }\ {g_0,p}) \nonumber\\ &\equiv [f]^l_{g_0} \cdot f \ (\mathrm{mod }\ {g_0,p}) \end{align} $$

(†) $$ \begin{align} &\equiv [f]^{l+1}_{g_0} \ (\mathrm{mod }\ {g_0,p}), \end{align} $$

where ( $\dagger $ ) follows from Lemma 4.20 and (*) follows from the induction hypothesis.

Lemma 4.22 ( $\mathrm {PV}_1$ , Composition of congruences)

Let p be a prime and let l and k be numbers, and let $f_1$ , $f_2$ and g be polynomials. If $f_1^l \equiv f_2 \ (\mathrm{mod }\ {g,p})$ then,

$$\begin{align*}(f_1^l)^k \equiv f_2^k \ (\mathrm{mod }\ {g,p}).\end{align*}$$

Proof. By induction on k. The case where $k=0$ is true trivially.

Assume the statement holds for k. Then by Lemma 4.20

$$ \begin{align*} (f_1^l)^{k+1} &\equiv (f_1^l)^{k} \cdot f_1^l\\ &\equiv f_2^{k} \cdot f_1^l\\ &\equiv f_2^{k} \cdot f_2 \equiv f_2^{k+1} \ (\mathrm{mod }\ {g,p}).\\[-39pt] \end{align*} $$

Proof. By Theorem 4.18, there is a polynomial $Q_r$ which divides ${\mathcal {X}}^r-1$ while satisfying $\gcd (Q_r,{\mathcal {X}}^{r'}-1)=1$ for any $0<r'<r$ . By Lemma 4.19 there is an irreducible factorization of $Q_r=\prod _{i=1}^k h_i$ . The $h=h_1$ satisfies that it is a divisor of ${\mathcal {X}}^r-1$ but not of any ${\mathcal {X}}^{r'}-1$ , where $0<r'<r$ . It remains to show that h is of degree at least $2$ .

Assume for contradiction that $\deg h=1$ , thus without loss of generality $h={\mathcal {X}}-\alpha $ , for some $\alpha \in \mathbb {Z}/p$ . By the $\text {GFLT}$ axiom, we have

$$\begin{align*}({\mathcal{X}}+\beta)^p \equiv {\mathcal{X}}^p+\beta \ (\mathrm{mod }\ {{\mathcal{X}}^r-1,p}),\end{align*}$$

for every $\beta \in \{0,\dots ,p-1\}$ . Since ${\mathcal {X}}-1\mid {\mathcal {X}}^r-1$ , Lemma 4.21 gives us

(*) $$ \begin{align} ({\mathcal{X}}+\beta)^p \equiv {\mathcal{X}}^p+\beta \ (\mathrm{mod }\ {{\mathcal{X}}-1,p}).{} \end{align} $$

We also trivially have

$$ \begin{align*} {\mathcal{X}} &\equiv 1 \ (\mathrm{mod }\ {{\mathcal{X}}-1,p})\\ {\mathcal{X}}+\beta &\equiv 1+\beta \ (\mathrm{mod }\ {{\mathcal{X}}-1,p}), \end{align*} $$

by Lemma 4.22, we have that

$$ \begin{align*} {\mathcal{X}}^p &\equiv 1^p \equiv 1 \ (\mathrm{mod }\ {{\mathcal{X}}-1,p})\\ ({\mathcal{X}}+\beta)^p &\equiv (1+\beta)^p \ (\mathrm{mod }\ {{\mathcal{X}}-1,p}), \end{align*} $$

which together with (*) gives us

$$\begin{align*}(1+\beta)^p \equiv 1+\beta \ (\mathrm{mod }\ {{\mathcal{X}}-1,p}).\end{align*}$$

Thus, by a linear substitution we have in $\mathbb {Z}/p$ that $\beta ^p = \beta $ , which implies $\beta ^{p-1}=1$ for every $\beta \in \{0,\dots ,p-1\}$ .

Since $p-1=qr+m$ , for some q and m, where $0< m < r$ , we have in $\mathbb {Z}/p$ that

$$\begin{align*}1 = \alpha^{p-1} = \alpha^{qr}\cdot \alpha^m = \alpha^m,\end{align*}$$

and $\alpha ^m \neq 1$ as this would imply by Lemma 4.23 that $h={\mathcal {X}}-\alpha $ divides ${\mathcal {X}}^m-1$ , which is a contradiction with the fact that h does not divide ${\mathcal {X}}^{r'}-1$ for any $0<r<r'$ .

4.3 The Root Upper Bound axiom

In the proof of Lemma G in [Reference Agrawal, Kayal and Saxena1], polynomials of degree polynomial in n are considered, as such they are not covered by the formalism of low degree polynomials. Polynomials with unrestricted degree can be defined over $\mathrm {PV}_1$ in a limited way as follows.

A sparse polynomial is a list of pairs of monomials and coefficients, with the intended meaning being the polynomial consisting of the sum of those monomials with those coefficients. Note that the number of monomials in a sparse polynomial is bounded by the length of the list, therefore by a length of some number. For sparse polynomials, we can define addition, multiplication and evaluation at an element of a bounded field in $\mathrm {PV}_1$ . We will also use the notation $\deg f$ to denote the highest exponent of a monomial in the sparse polynomial f. In the rest of this section, we define the second algebraic axiom needed for our formalization which facilitates reasoning about sparse polynomials. It uses a new function symbol to provide the injection replacing the inequality between the number of roots of a polynomial over a field and the degree of the polynomial.

Definition 4.25 (Root Upper Bound)

Let $\mathrm {PV}(\iota )$ denote the language of $\mathrm {PV}$ extended by a new ternary function symbol $\iota $ . The axiom $\mathrm {RUB}$ is the universal $\mathrm {PV}(\iota )$ -sentence naturally formalizing the following statement.

The injective function obtained from $\iota $ by fixing a bounded field F and a sparse polynomial $f\in F[{\mathcal {X}}]$ will be denoted $\iota _{F,f}$ .

Since the axiom $\mathrm {RUB}$ introduces a new function symbol, we need to extend the axiom schemas to allow this new function symbol in the formulas that appear in them.

5.1 $\mathrm {PV}_1\vdash $ Legendre’s formula

We start by proving Legendre’s formula in $\mathrm {PV}_1$ ; this is subsequently used to prove our variant of Lemma C — a lower bound on the value of $\text {lcm}(1,\dots ,2n)$ which is then used to prove our variant of Lemma D.

The following two Lemmas are straightforward and thus we omit their proofs.

Lemma 5.1. There is a binary $\mathrm {PV}$ -symbol $\nu _p(x)$ for which $\mathrm {PV}_1$ proves

$$ \begin{align*} \nu_p(0) &= 0\\ \nu_p(x)&=\begin{cases} \nu_p(\left \lfloor {x/p} \right\rfloor)+ 1 & x \equiv 0 \ (\mathrm{mod }\ {p}) \\ 0 & \text{otherwise.} \end{cases} \end{align*} $$

The value for $\nu _p(0)$ is often assigned to be $\infty $ , but since we never use $0$ as an argument, we simply defined it to be $0$ to keep the function total.

The following lemma defines the bit-length factorial.

Lemma 5.2. There is a $\mathrm {PV}$ -symbol $\text {Fact}({x})$ for which $\mathrm {PV}_1$ proves

$$ \begin{align*} \text{Fact}({0}) &= 1,\\ \text{Fact}({x}) &= \text{Fact}({\left \lfloor {x/2} \right\rfloor})\cdot {\lvert {x} \rvert}, \end{align*} $$

that is:

$$\begin{align*}\mathbb{N} \models \text{Fact}({x}) = {\lvert {x} \rvert}!\end{align*}$$

Proof. Assume that p is a prime, and . Then by the fact that p is prime we have $\gcd (x,p)=1$ and $\text {xgcd}(x,p)=(1,u,v)$ such that $ux+vp=1$ . Hence, $uxy+vpy = y$ and

$$\begin{align*}y\equiv (uxy+vpy) \equiv uxy \equiv 0 \ (\mathrm{mod }\ {p}).\\[-35pt] \end{align*}$$

Proof. We will first use induction on the formula $\psi _1(x)$ :

$$\begin{align*}i\leq \nu_p(x) \to p^i \mid x.\end{align*}$$

The case where $i=0$ is trivial. Assume $\psi (i)$ and $i+1\leq \nu _p(x)$ . By the inductive definition of $\nu _p(x)$ , the case where $p^{i}\mid x$ but $p^{i+1}\nmid x$ is contradictory.

We will now use induction on the formula $\psi _2(x)$ :

$$\begin{align*}p^i \mid x \to \nu_p(x)=i+\nu_p(\left \lfloor {x/p^{i}} \right\rfloor).\end{align*}$$

Again, the case where $i=0$ is trivial. Assume $\psi (i)$ and $p^{i+1}\mid x$ , then

(†) $$ \begin{align} \nu_p(x)&=i+\nu_p(\left \lfloor {x/p^{i}} \right\rfloor) \end{align} $$

(‡) $$ \begin{align} &=i+1+\nu_p(\left \lfloor {x/p^{i+1}} \right\rfloor). \end{align} $$

where ( $\dagger $ ) follows from the induction hypothesis, and ( $\ddagger $ ) follows from the definition of $\nu _p$ .

Together, we have established that

(*) $$ \begin{align}(\forall i)(i\leq \nu_p(x) \leftrightarrow p^i \mid x).\end{align} $$

Let $k=\nu _p(x)$ and $x'=\left \lfloor {x/p^{k}} \right \rfloor $ . From $(*)$ we get that $p^k \mid x$ , thus $x=x'p^k$ . Finally, if $p\mid x'$ , then $p^{k+1}\mid x'p^{k}=x$ , which by $(*)$ implies that $k=k+1$ , a contradiction.

Proof. By Lemma 5.4 there is $x'$ which is not divisible by p, such that $x=x'p^{k}$ , where $k=\nu _p(p)$ . We will proceed by induction on i on the formula

$$\begin{align*}\nu_p(x'yp^i)=i.\end{align*}$$

Assume that $i=0$ . Since $p\nmid x'$ and $p\nmid y$ , then by Lemma 5.3 $p\nmid x'y$ , and thus $\nu _p(x'y) = 0$ .

Now assume that $\nu _p(x'yp^i)=i$ , then

$$\begin{align*}\nu_p(x'yp^{i+1})=\nu_p(\left \lfloor {x'yp^{i+1}/p} \right\rfloor)+1 = \nu_p(x'yp^i)+1 = i+1,\end{align*}$$

which completes the induction step. By putting $i=k$ , we get that

$$\begin{align*}\nu_p(xy) =\nu_p(x'yp^{k})=k=\nu_p(x).\\[-40pt]\end{align*}$$

Lemma 5.6 ( $\mathrm {PV}_1$ )

For a prime p and $x,y>0$ we have

$$\begin{align*}\nu_p(x\cdot y) = \nu_p(x) + \nu_p(y).\end{align*}$$

Proof. By Lemma 5.4 there are $x'$ and $y'$ not divisible by p such that

$$\begin{align*}x=x'p^{\nu_p(x)},\quad y=y'p^{\nu_p(y)}.\end{align*}$$

Then

$$\begin{align*}\nu_p(xy) = \nu_p(x'y'p^{\nu_p(x)+\nu_p(y)})=\nu_p(x)+\nu_p(y),\end{align*}$$

where the last equality follows from Lemma 5.5.

Lemma 5.7 ( $\mathrm {PV}_1$ )

For every $1^{(n)}$ and a prime p we have

$$\begin{align*}\nu_p(\text{Fact}({1^{(n)}})) = \sum_{i=1}^n \nu_p(i).\end{align*}$$

Proof. By induction on n. The case $n=0$ is obvious.

Assume the statement holds for n, then by Lemma 5.6:

$$ \begin{align*} \nu_p(\text{Fact}({1^{(n+1)}})) &= \nu_p(\text{Fact}({1^{(n)}})\cdot (n+1))\\ &= \nu_p(\text{Fact}({1^{(n)}}))+\nu_p(n+1)\\ &= \sum_{i=1}^n \nu_p(i)+\nu_p(n+1)\\ &= \sum_{i=1}^{n+1} \nu_p(i).\\[-42pt] \end{align*} $$

Lemma 5.8 ( $\mathrm {PV}_1$ )

Let p be a prime and x be a number, then

$$\begin{align*}\nu_p(x) = \sum_{1\leq j\leq {\lvert {x} \rvert},\:p^j\mid x} 1.\end{align*}$$

Proof. By Lemma 5.4 there is $x'$ such that $x=x'p^{\nu _p(x)}$ . We will proceed by induction on the formula

$$\begin{align*}\nu_p(x'p^i) = \sum_{1\leq j \leq i;\:p^j \mid x} 1.\end{align*}$$

The case where $i=0$ is trivial. Assume that the statement holds for i. Then, $\nu _p(x'p^{i+1}) = \nu _p(x'p^i)+1=i+1,$ which completes the induction step. The statement of the lemma is obtained by taking $i=\nu _p(x)$ .

Lemma 5.9 ( $\mathrm {PV}_1$ )

Let $1^{(a)}$ and b be numbers, and $b\neq 0$ . Then

$$\begin{align*}\sum_{i=1,b\mid i}^a 1 = \left \lfloor {a/b} \right\rfloor.\end{align*}$$

Proof. By induction on a. The case where $a=0$ is trivial.

Assume that

$$\begin{align*}\sum_{i=1,b\mid i}^a 1 = \left \lfloor {a/b} \right\rfloor,\end{align*}$$

if $b\mid a+1$ , then

$$\begin{align*}\sum_{i=1,b\mid i}^{a+1} 1 = 1+ \sum_{i=1,b\mid i}^{a} 1 = 1+\left \lfloor {a/b} \right\rfloor = \left \lfloor {(a+1)/b} \right\rfloor,\end{align*}$$

and if $b\nmid a+1$ , then

$$\begin{align*}\sum_{i=1,b\mid i}^{a+1} 1 = \sum_{i=1,b\mid i}^{a} 1 =\left \lfloor {a/b} \right\rfloor = \left \lfloor {(a+1)/b} \right\rfloor.\\[-42pt]\end{align*}$$

We are now ready to prove Legendre’s formula in $\mathrm {PV}_1$ . Our proof is a direct adaptation of a standard proof.

Theorem 5.10 ( $\mathrm {PV}_1$ , Legendre’s formula)

For every $1^{(n)}$ and a prime p we have

$$\begin{align*}\nu_p(\text{Fact}({1^{(n)}})) = \sum_{i=1}^{\lvert {n} \rvert} \left \lfloor {n/p^i} \right\rfloor.\end{align*}$$

Proof. By direct computation:

(A) $$ \begin{align} \nu_p(\text{Fact}({1^{(n)}}))&=\sum_{j=1}^n \nu_p(j) \end{align} $$

(B) $$ \begin{align} &=\sum_{j=1}^n \sum_{i,p^i\mid j}1\end{align} $$

(C) $$ \begin{align} &= \sum_{i=1}^{{\lvert {n} \rvert}}\sum_{1\leq j\leq n; p^i \mid j} 1 \nonumber\\ &= \sum_{i=1}^{{\lvert {n} \rvert}} \left \lfloor {n/p^i} \right\rfloor, \end{align} $$

where (A) follows from Lemma 5.7, (B) follows from Lemma 5.8 and (C) follows from Lemma 5.9.

5.2 Lemma C

Proof. By $\Sigma ^b_1\text {-LMIN}$ we have

$$\begin{align*}(\forall n)(\exists m\leq n )(\forall m' \leq n)((1<n \land {\lvert {m'} \rvert} < {\lvert {m} \rvert}) \to (1< m \land m \mid n \land m' \nmid n)).\end{align*}$$

Let $n>1$ be a number, then we obtain m by the above formula. If m is not a prime, then there is $m'\mid m$ , $1<m'$ and ${\lvert {m'} \rvert }<{\lvert {m} \rvert }$ , which is in contradiction with the formula.

Proof. Assume that n and m satisfy that $\nu _p(n)\leq \nu _p(m)$ for every prime $p \leq n$ . Let $n'=\left \lfloor {n/\gcd (m,n)} \right \rfloor $ and $m' = \left \lfloor {m/\gcd (m,n)} \right \rfloor $ . If $n'=1$ then $n\mid m$ , and we are done. We now prove that $n'>1$ is impossible.

Assume for contradiction that $n'> 1$ , therefore by Lemma 5.11 there is a prime p such that $p\mid n'$ and therefore $p \mid n$ . If $\nu _p(m')>0$ , then $\gcd (m,n)\cdot p$ is a common divisor of both m and n, a contradiction with $\gcd (m,n)$ being the greatest common divisor. Therefore, we obtain that $\nu _p(m')=0$ .

Let $k=\nu _p(\gcd (m,n))$ . Then by Lemma 5.6,

$$ \begin{align*} \nu_p(n) = \nu_p(n' \cdot \gcd(m,n)) \geq k + 1>k + 0 = \nu_p(m'\cdot \gcd(m,n)) = \nu_p(m) \end{align*} $$

a contradiction.

Proof. Let p be a prime. By Lemma 5.6 and Theorem 5.10 we have

$$\begin{align*}\nu_p(\text{Fact}({1^{(n)}})^2)=2\cdot\sum_{i=1}^{\lvert {n} \rvert} \left \lfloor {n/p^i} \right\rfloor.\end{align*}$$

Again by Theorem 5.10

$$ \begin{align*} \nu_p(\text{Fact}({1^{(2n)}}))&=\sum_{i=1}^{{\lvert {2n} \rvert}}\left \lfloor {2n/p^i} \right\rfloor\\ &\geq\sum_{i=1}^{{\lvert {2n} \rvert}}2\cdot\left \lfloor {n/p^i} \right\rfloor\\ &\geq \nu_p(\text{Fact}({1^{(n)}})^2), \end{align*} $$

which by Lemma 5.12 gives $\text {Fact}({1^{(n)}})^2\mid \text {Fact}({1^{(2n)}})$ .

Lemma 5.14. There is a $\mathrm {PV}$ -symbol $\text {lcm}(\langle x_1,\dots ,x_m\rangle )$ , such that $\mathrm {PV}_1$ proves

$$\begin{align*}(\forall i\le m) \ (x_i \mid \text{lcm}(\langle x_1,\dots,x_m \rangle))\end{align*}$$

and

$$\begin{align*}(\forall y)((\forall i \leq m)( x_i \mid y) \to \text{lcm}(\langle x_1,\dots,x_m \rangle ) \mid y).\end{align*}$$

Proof

(Sketch). We can see that by putting

$$\begin{align*}\text{lcm}(\langle x_1,\dots,x_m\rangle ) = \begin{cases} 1 & m=0,\\ 0 & \exists 1\leq i \leq m: x_i=0,\\ \left \lfloor {\frac{\text{lcm}(\langle x_1,\dots, x_{m-1}\rangle )\cdot x_m }{\gcd(\text{lcm}(\langle x_1,\dots, x_{m-1}\rangle) ,x_m)}} \right\rfloor & \text{otherwise,} \end{cases}\end{align*}$$

the required properties are satisfied.

Lemma 5.15 ( $S^1_2$ )

For every $1^{(n)}$ , we have

$$\begin{align*}\left \lfloor {\text{Fact}({1^{(2n)}})/\text{Fact}({1^{(n)}})^2} \right\rfloor\mid \text{lcm}(1,\dots,2n).\end{align*}$$

Proof. Let p be a prime. By the length minimization principle for open $\mathrm {PV}$ -formulasFootnote ³ , there is a minimal r such that $2n < p^{r+1}$ . Notice that $r<{\lvert {n} \rvert }+1$ and that $p^r\leq 2n$ .

By Lemma 5.13 we have

$$\begin{align*}\text{Fact}({1^{(2n)}})= \left \lfloor {\text{Fact}({1^{(2n)}})/\text{Fact}({1^{(n)}})^2} \right\rfloor\cdot\text{Fact}({1^{(n)}})^2,\end{align*}$$

thus by Lemma 5.6

$$\begin{align*}\nu_p(\left \lfloor {\text{Fact}({1^{(2n)}})/\text{Fact}({1^{(n)}})^2} \right\rfloor) = \nu_p(\text{Fact}({1^{(2n)}}))- 2 \cdot \nu_p(\text{Fact}({1^{(n)}})).\end{align*}$$

Now by Theorem 5.10 we have

(*) $$ \begin{align} \nu_p(\left \lfloor {\text{Fact}({1^{(2n)}})/\text{Fact}({1^{(n)}})^2} \right\rfloor) &= \sum_{i=1}^{{\lvert {2n} \rvert}} \left \lfloor {2n/p^i} \right\rfloor - 2 \sum_{i=1}^{{\lvert {n} \rvert}}\left \lfloor {n/p^i} \right\rfloor \nonumber\\ &= \sum_{i=1}^{{\lvert {n} \rvert}+1} \left \lfloor {2n/p^i} \right\rfloor - 2 \sum_{i=1}^{{\lvert {n} \rvert}}\left \lfloor {n/p^i} \right\rfloor \nonumber\\ &= \sum_{i=1}^{r} \left \lfloor {2n/p^i} \right\rfloor - 2 \sum_{i=1}^{r}\left \lfloor {n/p^i} \right\rfloor \end{align} $$

(†) $$ \begin{align} &= \sum_{i=1}^{r} (\left \lfloor {2n/p^i} \right\rfloor - 2\left \lfloor {n/p^i} \right\rfloor) \nonumber\\ &\leq r, \end{align} $$

where (*) follows because $\left \lfloor {2n/p^i} \right \rfloor =0$ for $i>r$ and $(\dagger )$ follows from the fact that $\left \lfloor {2n/p^i} \right \rfloor -2\left \lfloor {n/p^i} \right \rfloor \leq 1$ for every $i\geq 0$ . By the fact that $p^r\leq 2n$ we have

$$\begin{align*}\nu_p(\text{lcm}(1,\dots,2n))\geq r\end{align*}$$

and therefore by Lemma 5.12 the statement follows.

Theorem 5.16 ( $S^1_2$ )

For every $1^{(n)}$ we have

$$\begin{align*}2^n \leq \text{lcm}(1,\dots,2n).\end{align*}$$

Proof. By Lemma 5.15 it is enough to prove $2^n \leq \left \lfloor {\text {Fact}({1^{(2n)}})/(\text {Fact}({1^{(n)}})^2)} \right \rfloor $ . We proceed by induction on n. For $n=1$ the statement holds as

$$\begin{align*}2^1 \leq 2!/(1!)^2= 2.\end{align*}$$

Assume the inequality holds for n. Then

$$ \begin{align*} \left \lfloor {\text{Fact}({1^{(2(n+1))}})/\text{Fact}({1^{(n+1)}})^2} \right\rfloor2&=\left \lfloor {\frac{\text{Fact}({1^{(2n)}})(2n+2)(2n+1)}{\text{Fact}({1^{(n)}})^2(n+1)^2}} \right\rfloor\\ &\geq\left \lfloor {\frac{\text{Fact}({1^{(2n)}})(2n+2)}{\text{Fact}({1^{(n)}})^2(n+1)}} \right\rfloor\\ &=2 \cdot \left \lfloor {\text{Fact}({1^{(2n)}})/(\text{Fact}({1^{(n)}})^2)} \right\rfloor\\ &\geq 2\cdot 2^n = 2^{n+1}.\\[-38pt] \end{align*} $$

Corollary 5.17 ( $S^1_2$ , Lemma C)

For every $1^{(m)}$ we have

$$\begin{align*}2^{\left \lfloor {m/2} \right\rfloor} \leq \text{lcm}(1,\dots, m).\end{align*}$$

5.3 Lemma D

The following Lemma defines order for multiplicative groups whose universe is bounded by a length. The restriction on the size makes all relevant arguments easily formalizable in $\mathrm {PV}_1$ and thus we omit its proof.

Lemma 5.18. There is a $\mathrm {PV}$ -symbol $\text {ORD}$ such that $\mathrm {PV}_1$ proves for every y and x satisfying ${\gcd (x,{\lvert {y} \rvert })=1}$ that

We will write $\text {ord}_r(y)$ to denote $\text {ORD}(y,1^{(r)})$ .

Proof. Notice, that $\text {ord}_r(x) = i$ implies $r \mid (x^i-1)$ . Let

$$\begin{align*}a = x^{b}\prod_{i=1}^{{\lvert {x} \rvert}^2}(x^i-1)< x \cdot x ^{{\lvert {x} \rvert}^4} < 2^{{\lvert {x} \rvert}^6},\end{align*}$$

where $b={\lvert {2{\lvert {x} \rvert }^6} \rvert }$ . By Corollary 5.17 we have

$$\begin{align*}2^{{\lvert {x} \rvert}^6} \leq \text{lcm}(1,\dots, 2\cdot {\lvert {x} \rvert}^6).\end{align*}$$

Hence, $\text {lcm}(1,\dots ,2\cdot {\lvert {x} \rvert }^6)$ does not divide a. By Lemma 5.14 we have that there is $r\leq 2 \cdot {\lvert {x} \rvert }^6$ such that r does not divide a, and since this value is bounded by a length, we can take the smallest such r.

We will show that $\gcd (r,x)=1$ . First, notice that from $r\leq 2{\lvert {x} \rvert }^6$ it follows that for any prime p that $\nu _p(r)\leq b$ . Also for any prime p we have that $\nu _p(x)\geq 1$ implies $\nu _p(x^b)\geq b$ .

Claim. There is a prime p such that $\nu _p(r)> \nu _p(a)$ and $\nu _p(x)=0$ .

Proof of claim. First, if $\nu _p(r)\geq 1$ and $\nu _p(x)\geq 1$ , then

$$\begin{align*}\nu_p(r)\leq b \leq \nu_p(x^b) \leq \nu_p(a).\end{align*}$$

Since $r\nmid a$ , then by Lemma 5.12 there is a prime p such that $\nu _p(r)>\nu _p(a)$ , which cannot happen if $\nu _p(x)\geq 1$ . This proves the claim.

Consider the value $r/\gcd (r,x)$ , we have

$$\begin{align*}\nu_p(r/\gcd(r,x)) = \nu_p(r)>\nu_p(a),\end{align*}$$

thus by Lemma 5.12 we have that $r/\gcd (r,x)\nmid a$ . Since r was chosen as the smallest nondivisor of a, then $\gcd (r,x)=1$ .

We claim that r has $\text {ord}_r(x)>{\lvert {x} \rvert }^2$ . If $\text {ord}_r(x)\leq {\lvert {x} \rvert }^2$ then there is $i\leq {\lvert {x} \rvert }^2$ such that

$$\begin{align*}r \mid (x^i-1) \mid \prod_{i=1}^{{\lvert {x} \rvert}^2}(x^i-1),\end{align*}$$

a contradiction.

This lemma implies, that the if statement on line 4 of the AKS algorithm is relevant only for finitely many values. The case of correctness where this if statement results in the answer COMPOSITE can be ignored, because it can be expressed a true bounded sentence and thus proved in $\mathrm {PV}_1$ .

5.4 Congruence Lemma

Let us denote by $H_0(n,r)$ the following assumptions: n is a number such that holds, i.e., the AKS algorithm asserts that n is prime, and r is the value provided by the algorithm satisfying $\text {ord}_r(n)> |n|^{2}$ .

We show that there is a prime divisor of n called p such that $\text {ord}_r(p)>1$ .

Let us fix p to be a prime divisor of n such that $\text {ord}_r(p)>1$ . The rest of Section 5 is dedicated to showing that n satisfies $\text {Prime}(n)$ . To prove the congruence lemma we will use two simple properties of exponentiation by squaring.

Lemma 5.22 ( $\mathrm {PV}_1$ , Evaluation lemma)

Let p be a prime, l be a number and let $f_1$ , $f_2$ and g be low degree polynomials. Then,

$$\begin{align*}[f_1^l](f_2) \equiv ([f_1](f_2))^l \ (\mathrm{mod }\ { [g](f_2),p}),\end{align*}$$

where $[g_1](g_2)$ denotes the composition of a polynomial $g_2$ with a polynomial $g_1$ .

Proof. By induction on l. The case where $l=0$ is true trivially.

Assume the statement holds for l. Then by Lemma 4.20

$$ \begin{align*} [f_1^{l+1}](f_2) &\equiv [f_1^l](f_2) \cdot [f_1](f_2)\\ &\equiv ([f_1](f_2))^l \cdot [f_1](f_2)\\ &\equiv ([f_1](f_2))^{l+1} \ (\mathrm{mod }\ {[g](f_2),p}).\\[-39pt] \end{align*} $$

Lemma 5.23 ( $\mathrm {PV}_1$ , Composition of exponentiation)

Let p be a prime and let l and k be numbers, and let f and g be low degree polynomials. Then,

$$\begin{align*}((f)^l)^k \equiv f^{l\cdot k} \ (\mathrm{mod }\ {g,p}).\end{align*}$$

Proof. By induction on k. The case where $k=0$ is true trivially.

Assume the statement holds for k. Then by Lemma 4.20

$$ \begin{align*} ((f)^l)^{k+1} &\equiv (f^l)^k \cdot f^l\\ &\equiv f^{l\cdot k} \cdot f^l\\ &\equiv f^{l\cdot k + l} \equiv f^{l\cdot (k+1)} \ (\mathrm{mod }\ {g,p}), \end{align*} $$

where the additivity of exponents also follows from Lemma 4.20 by straightforward induction.

Lemma 5.24 ( $S^1_2+\text {GFLT}$ , Congruence Lemma)

Assuming $H_0(n,r)$ and a being a number such that $\gcd (a,p)=1$ , we have:

$$\begin{align*}({\mathcal{X}}+a)^{\frac{n}{p}} \equiv {\mathcal{X}}^{\frac{n}{p}}+a \ (\mathrm{mod }\ {{\mathcal{X}}^r-1, p}). \end{align*}$$

Proof. By the notation $x \equiv y$ , we mean $x\equiv y \ (\mathrm{mod }\ {{\mathcal {X}}^r-1, p})$ throughout this proof. By we have $({\mathcal {X}}+a)^n \equiv {\mathcal {X}}^n+a \ (\mathrm{mod }\ {{\mathcal {X}}^r-1,n})$ . We have

(1) $$ \begin{align} ({\mathcal{X}}+a)^n \equiv {\mathcal{X}}^n+a\end{align} $$

(2) $$ \begin{align} ({\mathcal{X}}+a)^p \equiv {\mathcal{X}}^p+a \end{align} $$

The equivalence $(1)$ follows from the fact that p is a prime divisor of n and $(2)$ is an instance of the axiom GFLT. Since $r < p$ and p is prime, there exist u and v such that $\text {xgcd}(r,p)=(1,u,v)$ . Thus, $pv \equiv 1 \ (\mathrm{mod }\ {r})$ . Without loss of generality, we can assume that $v>0$ , because otherwise, we can take $v' = v -rv>0$ . Since ${\mathcal {X}}^v$ is a low degree polynomial (as $v <r$ ), by substituting ${\mathcal {X}}^v$ for ${\mathcal {X}}$ in $(1)$ using Lemma 4.21 and Lemma 5.22 we get

$$\begin{align*}({\mathcal{X}}^v+a)^n \equiv {\mathcal{X}}^{v \cdot n}+a. \end{align*}$$

To be concrete, by (1) we have:

(3) $$ \begin{align}[{\mathcal{X}}+a]_{{\mathcal{X}}^{r}-1}^{n}\equiv[{\mathcal{X}}]_{{\mathcal{X}}^{r}-1}^{n}+a\ (\mathrm{mod }\ {{\mathcal{X}}^{r}-1,p})\end{align} $$

By substituting ${\mathcal {X}}^v$ we get

(4) $$ \begin{align}[{\mathcal{X}}+a]_{{\mathcal{X}}^{r}-1}^{n}({\mathcal{X}}^{v})\equiv[{\mathcal{X}}]_{{\mathcal{X}}^{r}-1}^{n}({\mathcal{X}}^{v})+a\ (\mathrm{mod }\ {{\mathcal{X}}^{vr}-1,p})\end{align} $$

By Lemma 5.22:

(5) $$ \begin{align} [{\mathcal{X}}+a]_{{\mathcal{X}}^{vr}-1}^{n}({\mathcal{X}}^{v})&\equiv[{\mathcal{X}}^{v}+a]_{{\mathcal{X}}^{vr}-1}^{n}\ (\mathrm{mod }\ {{\mathcal{X}}^{vr}-1,p})\end{align} $$

(6) $$ \begin{align} [{\mathcal{X}}]_{{\mathcal{X}}^{vr}-1}^{n}({\mathcal{X}}^{v})&\equiv[{\mathcal{X}}^{v}]_{{\mathcal{X}}^{vr}-1}^{n}\ (\mathrm{mod }\ {{\mathcal{X}}^{vr}-1,p}) \end{align} $$

By Lemma 4.21:

(7) $$ \begin{align} [{\mathcal{X}}^{v}+a]_{{\mathcal{X}}^{vr}-1}^{n}&\equiv[{\mathcal{X}}^{v}+a]_{{\mathcal{X}}^{r}-1}^{n}\ (\mathrm{mod }\ {{\mathcal{X}}^{r}-1,p})\end{align} $$

(8) $$ \begin{align} [{\mathcal{X}}+a]_{{\mathcal{X}}^{vr}-1}^{n}&\equiv[{\mathcal{X}}+a]_{{\mathcal{X}}^{r}-1}^{n}\ (\mathrm{mod }\ {{\mathcal{X}}^{r}-1,p}) \end{align} $$

(9) $$ \begin{align} [{\mathcal{X}}^{v}]_{{\mathcal{X}}^{vr}-1}^{n}&\equiv[{\mathcal{X}}^{v}]_{{\mathcal{X}}^{r}-1}^{n}\ (\mathrm{mod }\ {{\mathcal{X}}^{r}-1,p}) \end{align} $$

(10) $$ \begin{align} [{\mathcal{X}}]_{{\mathcal{X}}^{vr}-1}^{n}&\equiv[{\mathcal{X}}]_{{\mathcal{X}}^{r}-1}^{n}\ (\mathrm{mod }\ {{\mathcal{X}}^{r}-1,p}) \end{align} $$

Therefore

(by (7)) $$ \begin{align} [{\mathcal{X}}^{v}+a]_{{\mathcal{X}}^{r}-1}^{n} &\equiv [{\mathcal{X}}^{v}+a]_{{\mathcal{X}}^{vr}-1}^{n} \end{align} $$

(by (5)) $$ \begin{align} &\equiv [{\mathcal{X}}+a]_{{\mathcal{X}}^{vr}-1}^{n}({\mathcal{X}}^{v})\end{align} $$

(by (8)) $$ \begin{align} &\equiv [{\mathcal{X}}+a]_{{\mathcal{X}}^{r}-1}^n({\mathcal{X}}^{v}) \end{align} $$

(by (4)) $$ \begin{align} &\equiv [{\mathcal{X}}]_{{\mathcal{X}}^{r}-1}^{n}({\mathcal{X}}^{v})+a \end{align} $$

(by (10)) $$ \begin{align} &\equiv [{\mathcal{X}}]_{{\mathcal{X}}^{vr}-1}^{n}({\mathcal{X}}^{v})+a\end{align} $$

(by (6)) $$ \begin{align} &\equiv [{\mathcal{X}}^v]_{{\mathcal{X}}^{vr}-1}^{n}+a \end{align} $$

(by (9)) $$ \begin{align} &\equiv [{\mathcal{X}}^v]_{{\mathcal{X}}^{r}-1}^{n}+a\ (\mathrm{mod }\ {{\mathcal{X}}^r-1,p}), \end{align} $$

or simply $({\mathcal {X}}^v+a)^n \equiv {\mathcal {X}}^{v \cdot n}+a$ . By an analogous argument, we can use (2), Lemma 4.21 and Lemma 5.22 to get

$$\begin{align*}({\mathcal{X}}^v+a)^p \equiv {\mathcal{X}}^{v \cdot p} +a \equiv {\mathcal{X}} +a. \end{align*}$$

By Lemma 5.23, we obtain

(*) $$ \begin{align} (({\mathcal{X}}^v+a)^p)^{\frac{n}{p}} \equiv {\mathcal{X}}^{v \cdot n}+a. \end{align} $$

Moreover, using Lemmas 4.22 and 5.23 we get:

$$\begin{align*}{\mathcal{X}}^{v \cdot n} \equiv {\mathcal{X}}^{v \cdot p \cdot \frac{n}{p}} \equiv ({\mathcal{X}}^{v \cdot p})^{\frac{n}{p}} \equiv {\mathcal{X}}^{\frac{n}{p}}. \end{align*}$$

Therefore, by Lemma 4.22, $(*)$ will become

$$\begin{align*}({\mathcal{X}}+a)^{\frac{n}{p}} \equiv {\mathcal{X}}^{\frac{n}{p}}+a.\\[-39pt] \end{align*}$$

5.5 Lemma E

To prove Lemma E, let us first fix some notation. Let p be a prime divisor of n such that $\text {ord}_r(p)>1$ . For the ease of notation, we will denote $\mathbb {Z}/p$ by $F_p$ . By Corollary 4.24, for $F_p[{\mathcal {X}}]$ and r, there exists an irreducible divisor h of ${\mathcal {X}}^r -1$ in $F_p[{\mathcal {X}}]$ such that $h \not \mid {\mathcal {X}}^{r'}-1$ for all $r' <r$ and $1< \deg (h) <r$ . Take such h and fix it and take $F= F_p[{\mathcal {X}}] / h({\mathcal {X}})$ . The following lemma introduces a set $G_r$ represented by a $\mathrm {PV}$ -predicate, which will be used in the rest of the paper.

Lemma 5.25. Assuming $H_0(n,r)$ , there is a $\mathrm {PV}$ -symbol $G_r(x)$ such that $\mathrm {PV}_1$ proves:

$$\begin{align*}G_r(x) \leftrightarrow (x <r) \wedge (\exists i, j\leq r) (x\equiv (n/p)^i \cdot p^j \ (\mathrm{mod }\ {r})). \end{align*}$$

We sometimes use the notation $m\in G_r$ to mean $G_r(m)$ . By Lemma 5.19, the number r is bounded by ${\lvert {n} \rvert }^{10}$ . The theory $\mathrm {PV}_1$ can assign a cardinality to sets bounded by a length (and $|m|^{10}$ is the length of $s(m)$ for a suitable term s). We denote the cardinality of the set $\{x; G_r(x)\}$ by t, where $t < r$ .

Proof. We already know

(*) $$ \begin{align} \quad \gcd(n,r)= \gcd(p,r)=1 \qquad \text{and hence} \qquad \gcd(n/p,r)=1 \end{align} $$

We claim that for any x such that $G_r(x)$ we have $\gcd (x,r)=1$ . As $G_r(x)$ , there exist $i,j \leq r$ such that $x\equiv (n/p)^i \cdot p^j \ (\mathrm{mod }\ {r})$ . Suppose for the sake of contradiction that $\gcd (x, r)=c$ where $c \neq 1$ . Thus,

$$\begin{align*}c \mid r \qquad \text{and} \qquad c \mid (n/p)^i \cdot p^j \end{align*}$$

If $i \leq j$ then $ c \mid (n/p)^{i-j}$ which is a contradiction with $\gcd (n/p,r)=1$ . If $i < j$ , then $c \mid n^i p^{j-i}$ , which is a contradiction with the left side of (*).

Lemma 5.27 ( $S^1_2$ )

Assume $H_0(n,r)$ . Let f be a sparse polynomial and m a number. There is a ternary $\mathrm {PV}$ -predicate $\mathrm {int}_{{\mathcal {X}}^r-1}(f,p,m)$ for which $S^1_2$ proves

$$\begin{align*}\mathrm{int}_{X^r-1}(f, p, m) \leftrightarrow \big(f({\mathcal{X}})\big)^m \equiv f({\mathcal{X}}^m)\ (\mathrm{mod }\ {{\mathcal{X}}^r-1, p}).\end{align*}$$

The number m is called introspective for $f({\mathcal {X}})$ .

Let us fix $\ell = \left \lfloor {\sqrt {\phi (r)}} \right \rfloor \cdot \left \lfloor {\text {log}\, n} \right \rfloor $ . We have the following easy observation.

The following lemma combines Lemmas 4.5 and 4.6 in [Reference Agrawal, Kayal and Saxena1]. It proves the closure of introspective numbers under multiplication and also shows that the set of polynomials for which m is introspective is closed under multiplication.

Proof. As m is introspective for $f({\mathcal {X}})$ we have by Lemma 4.22 and Lemma 5.23:

(†) $$ \begin{align} \big(f({\mathcal{X}})\big)^{m \cdot m'} \equiv \big(f({\mathcal{X}}^m)\big)^{m'}\ (\mathrm{mod }\ {{\mathcal{X}}^r-1, p}) . \end{align} $$

Let $m = q\cdot r + m_r$ , where $0\leq m_r<r$ . Then, by Lemma 4.20, Lemma 4.22, Lemma 5.23, and ${\mathcal {X}}^r \equiv 1 \ (\mathrm{mod }\ {{\mathcal {X}}^r-1,p})$ , we have:

$$\begin{align*}{\mathcal{X}}^m \equiv {\mathcal{X}}^{q \cdot r +m_r} \equiv {\mathcal{X}}^{q\cdot r} {\mathcal{X}}^{m_r} \equiv ({\mathcal{X}}^r)^q {\mathcal{X}}^{m_r} \equiv 1^q \cdot {\mathcal{X}}^{m_r} \equiv {\mathcal{X}}^{m_r} \ (\mathrm{mod }\ {{\mathcal{X}}^r-1, p}), \end{align*}$$

which implies by Lemma 5.23

$$\begin{align*}{\mathcal{X}}^{m_r\cdot m'} \equiv ({\mathcal{X}}^{m_r})^{m'}\equiv ({\mathcal{X}}^{m})^{m'} \equiv {\mathcal{X}}^{m\cdot m'} \ (\mathrm{mod }\ {{\mathcal{X}}^r-1,p}).\end{align*}$$

By Lemma 5.22 we have

(A) $$ \begin{align} [f({\mathcal{X}}^{m_r})]_{{\mathcal{X}}^{m_r\cdot r}-1}^{m'}&\equiv [f]^{m'}_{{\mathcal{X}}^{m_r\cdot r}-1}({\mathcal{X}}^{m_r}) \ (\mathrm{mod }\ {{\mathcal{X}}^{m_r\cdot r}-1}) \end{align} $$

(B) $$ \begin{align} [{\mathcal{X}}^{m_r}]^{m'}_{{\mathcal{X}}^{m_r\cdot r}-1} &\equiv [{\mathcal{X}}]^{m'}_{{\mathcal{X}}^{m_r\cdot r}-1}({\mathcal{X}}^{m_r}) \ (\mathrm{mod }\ {{\mathcal{X}}^{m_r \cdot r}-1}). \end{align} $$

As ${\mathcal {X}}^r-1 \mid {\mathcal {X}}^{m_r\cdot r}-1$ , by Lemma 4.21:

$$ \begin{align*} [f]_{{\mathcal{X}}^{m_r\cdot r}-1}^{m'} &\equiv [f]^{m'}_{{\mathcal{X}}^{r}-1}\ (\mathrm{mod }\ {{\mathcal{X}}^r-1,p})\\ [{\mathcal{X}}]^{m'}_{{\mathcal{X}}^{m_r\cdot r}-1} &\equiv [{\mathcal{X}}]^{m'}_{{\mathcal{X}}^{r}-1} \ (\mathrm{mod }\ {{\mathcal{X}}^{r}-1,p}). \end{align*} $$

Moreover, by general algebra

(C) $$ \begin{align} [f]_{{\mathcal{X}}^{m_r\cdot r}-1}^{m'}({\mathcal{X}}^{m_r}) &\equiv [f]^{m'}_{{\mathcal{X}}^{r}-1}({\mathcal{X}}^{m_r})\ (\mathrm{mod }\ {{\mathcal{X}}^{m_r\cdot r}-1,p}) \end{align} $$

(D) $$ \begin{align}[{\mathcal{X}}]^{m'}_{{\mathcal{X}}^{m_r\cdot r}-1}({\mathcal{X}}^{m_r}) &\equiv [{\mathcal{X}}]^{m'}_{{\mathcal{X}}^{r}-1}({\mathcal{X}}^{m_r}) \ (\mathrm{mod }\ {{\mathcal{X}}^{m_r\cdot r}-1,p}). \end{align} $$

By the introspectivity of $m'$

$$\begin{align*}[f]^{m'}_{{\mathcal{X}}^r-1} \equiv f([{\mathcal{X}}]^{m'}_{{\mathcal{X}}^r-1}) \ (\mathrm{mod }\ {{\mathcal{X}}^r-1,p}).\end{align*}$$

Then,

$$\begin{align*}[f]^{m'}_{{\mathcal{X}}^r-1}({\mathcal{X}}^{m_r}) \equiv f([{\mathcal{X}}]^{m'}_{{\mathcal{X}}^r-1})({\mathcal{X}}^{m_r}) \ (\mathrm{mod }\ {{\mathcal{X}}^{m_r\cdot r}-1,p}).\end{align*}$$

By (C) and (A)

$$\begin{align*}[f]^{m'}_{{\mathcal{X}}^{r}-1}({\mathcal{X}}^{m_r}) \equiv [f]_{{\mathcal{X}}^{m_r\cdot r}-1}^{m'}({\mathcal{X}}^{m_r}) \equiv [f({\mathcal{X}}^{m_r})]_{{\mathcal{X}}^{m_r\cdot r}-1}^{m'} \ (\mathrm{mod }\ {{\mathcal{X}}^{m_r\cdot r}-1,p}),\end{align*}$$

and by (D) and (B)

$$ \begin{align*} f([{\mathcal{X}}]^{m'}_{{\mathcal{X}}^r-1})({\mathcal{X}}^{m_r}) &\equiv f([{\mathcal{X}}]^{m'}_{{\mathcal{X}}^{m_r\cdot r}-1}({\mathcal{X}}^{m_r}))\\ &\equiv f([{\mathcal{X}}^{m_r}]^{m'}_{{\mathcal{X}}^{m_r\cdot r}-1}) \ (\mathrm{mod }\ {{\mathcal{X}}^{m_r\cdot r}-1,p}). \end{align*} $$

Therefore, we have

$$\begin{align*}{\big(f({\mathcal{X}}^{m_r})\big)^{m'} } \equiv {f(({\mathcal{X}}^{m_r})^{m'}}) \ (\mathrm{mod }\ {{\mathcal{X}}^{m_r \cdot r}-1,p}).\end{align*}$$

Thus, by ${\mathcal {X}}^r-1 \mid {\mathcal {X}}^{m_r\cdot r}-1$ and Lemma 4.21 we have

$$\begin{align*}{\big(f({\mathcal{X}}^{m_r})\big)^{m'} } \equiv f({\mathcal{X}}^{m_r\cdot m'})\ (\mathrm{mod }\ {{\mathcal{X}}^{r}-1,p}).\end{align*}$$

By ( $\dagger $ ) we get $m \cdot m'$ is introspective for $f({\mathcal {X}})$ :

$$ \begin{align*} \big(f({\mathcal{X}})\big)^{m \cdot m'} \equiv (f({\mathcal{X}}^m))^{m'} &\equiv (f({\mathcal{X}}^{m_r}))^{m'}\\ &\equiv f({\mathcal{X}}^{m_r\cdot m'}) \equiv f({\mathcal{X}}^{m \cdot m'})\ (\mathrm{mod }\ {{\mathcal{X}}^r-1, p}). \end{align*} $$

For the second part of the lemma, by Lemma 4.20 we have:

$$ \begin{align*}{\big(f({\mathcal{X}}) \cdot g({\mathcal{X}})\big)^m } \equiv \big(f({\mathcal{X}})\big)^m \cdot \big(g({\mathcal{X}})\big)^m \equiv f({\mathcal{X}}^m) \cdot g({\mathcal{X}}^m)\ (\mathrm{mod }\ {{\mathcal{X}}^r-1, p}).\\[-39pt]\end{align*} $$

5.6 Lemma F

Recall that $H_0(n,r)$ denotes the following assumptions: n is a number such that holds, i.e., the AKS algorithm asserts that n is prime, and r is the value provided by the algorithm satisfying $\text {ord}_r(n)> |n|^{2}$ . From now on, we let $H(n,r)$ denote the assumption $H_0(n,r)$ extended by fixing the following values:

• • $\ell = \left \lfloor {\sqrt {\phi (r)}} \right \rfloor \cdot \left \lfloor {\text {log}\, n} \right \rfloor $ ;

• • $t=|G_r|$ ;

• • p as a prime divisor of n such that $\text {ord}_r(p)>1$ ;

• • $F_p=\mathbb {Z}/p$ ;

• • an irreducible divisor h of ${\mathcal {X}}^r -1$ in $F_p[{\mathcal {X}}]$ such that $h \not \mid {\mathcal {X}}^{r'}-1$ for all $r' <r$ and $1< \deg (h) <r$ ;

• • $F= F_p[{\mathcal {X}}] / h({\mathcal {X}})$ .

Recall that $G_r$ is the set introduced in Lemma 5.25. We start with an easy observation about $G_r$ .

Lemma 5.30 ( $S^1_2+\text {GFLT}$ )

Assume $H(n,r)$ . For any distinct elements m and $m'$ of $G_r$ we have

Proof. We prove the lemma by contraposition. Suppose

$$\begin{align*}{\mathcal{X}}^m \equiv {\mathcal{X}}^{m'} \ (\mathrm{mod }\ {h({\mathcal{X}}), p}). \end{align*}$$

Then, $h \mid {\mathcal {X}}^{m'}-{\mathcal {X}}^m$ and hence

$$\begin{align*}h \mid {\mathcal{X}}^{m} \cdot ({\mathcal{X}}^{m'-m}-1). \end{align*}$$

However, since $m'<r$ and $m \neq m'$ , by Corollary 4.24 we have

$$\begin{align*}h \not \mid {\mathcal{X}}^{m'-m}-1. \end{align*}$$

Therefore, $h \mid {\mathcal {X}}^m$ . Since h is an irreducible polynomial, this means that $h({\mathcal {X}})={\mathcal {X}}$ . However, this contradicts the fact that $\deg (h)>1$ . Thus, we must have $m=m'$ .

The following are a series of lemmas necessary for the proof of Lemma F. To state the next lemma, we use the $\mathrm {PV}$ -symbol $\text {NumOnes}(x)$ which counts the number of ones in the binary expansion of its argument.

Lemma 5.31 ( $\mathrm {PV}_1$ )

There is a $\mathrm {PV}$ -symbol $c_{k}^{m}(x)$ such that $\mathrm {PV}_1$ proves for any numbers $1^{(k)}$ and $1^{(m)}$

$$\begin{align*}c_k^m(x) \leftrightarrow |x| \leq m \wedge \text{NumOnes}(x)=k. \end{align*}$$

Lemma 5.32 ( $\mathrm {PV}_1$ )

There is a $\mathrm {PV}$ -symbol $f_{k}^m(i)$ such that $\mathrm {PV}_1$ proves for any numbers $1^{(k)}$ and $1^{(m)}$ , where $0 \leq k \leq m$ ,

$$\begin{align*}f_{k}^m: \left\{0<i \leq \binom{m}{k}\right\} \to \{x; c_k^m(x)=1\}, \end{align*}$$

is an injective function.

Proof. By recursion (simultaneously on k and m) define the function $f_k^m$ as:

$$\begin{align*}f^0_0(1)=0 \quad \text{and} \quad f_k^{m+1}(i) = \begin{cases} f_k^{m}(i) & 0 < i \leq \binom{m}{k} \\ f_{k-1}^{m}(i-\binom{m}{k})+2^m & \binom{m}{k} < i \leq \binom{m+1}{k} \end{cases} \end{align*}$$

Now, we prove the following claim.

Claim. If $0 < i \leq \binom {m+1}{k}$ then we have $c_k^{m+1}(f_k^{m+1}(i))$ .

We prove the claim by induction on k and m. For $k=m=0$ the claim trivially holds. Suppose by the induction step, for any $0 < i \leq \binom {m+1}{k}$ , we have $c_k^{m}(f_k^m (i))$ and $c_{k-1}^{m}(f_{k-1}^m (i))$ . Using the equality $\binom {m+1}{k}= \binom {m}{k}+ \binom {m}{k-1}$ and the definition of the predicate $c_k^{m+1}(x)$ , it is easy to see that the following holds for any $x < 2^{m+1}$

(*) $$ \begin{align} c_k^{m+1}(x)= c_k^{m}(x) \vee c_k^{m}(2^m+x) \end{align} $$

Now, if $0 < i \leq \binom {m+1}{k}$ then either $i \leq \binom {m}{k}$ or $\binom {m}{k} < i \leq \binom {m+1}{k}$ .

• • If $0 < i \leq \binom {m}{k}$ , we have $f^{m+1}_k(i)=f^m_k(i)$ and by the induction step we have $c_k^m(f^m_k(i))$ . By (*), we get $c_k^{m+1}(f^m_k(i))$ .

• • If $\binom {m}{k} < i \leq \binom {m+1}{k}$ , we have $f_{k}^{m+1}(i)= f_{k-1}^{m}(i-\binom {m}{k})+2^m$ . By the induction step, $c_{k-1}^{m}(f_{k-1}^m (i-\binom {m}{k}))$ . Therefore, we get $c_{k}^{m+1}(f_{k-1}^m (i-\binom {m}{k})+2^m)$ and hence, by (*), we get $c_{k}^{m+1}(f_{k}^{m+1} (i))$ .

This finishes the proof of the claim. Now, it remains to prove that $f_k^m$ is injective. By induction on k and m we prove that if $f_{k}^{m+1}(i)=f_{k}^{m+1}(j)$ then $i=j$ . By the induction step, we know that

$$\begin{align*}\text{if} \; f_{k}^{m}(i)=f_{k}^{m}(j)\; \text{then} \; i=j \qquad \text{if} \; f_{k-1}^{m}(i)=f_{k-1}^{m}(j)\; \text{then} \; i=j \end{align*}$$

There are three cases:

1. 1. If $i,j \leq \binom {m}{k}$ , then $f_{k}^{m+1}(i)=f_{k}^{m+1}(j)=f_{k}^{m}(i)=f_{k}^{m}(j)$ . Therefore, by the induction step, we have $i=j$ .

2. 2. If $\binom {m}{k} < i,j \leq \binom {m+1}{k}$ , then $f_{k}^{m+1}(i)=f_{k}^{m+1}(j)=f_{k-1}^{m}(i-\binom {m}{k})+2^m=f_{k-1}^{m}(j-\binom {m}{k})+2^m$ . Again, by the induction step, we have $i=j$ .

3. 3. We show that the case where $i \leq \binom {m}{k}$ and $\binom {m}{k} <j \leq \binom {m+1}{k}$ is not possible. For the sake of contradiction, suppose otherwise. Then,

   $$ \begin{align*} f_{k}^{m+1}(i) & =f_{k}^{m+1}(j) & \text{(By the assumption)} \\ f_{k}^{m+1}(i) & =f_{k}^{m}(i) & \text{as} \; i \leq \binom{m}{k} \\ f_{k}^{m+1}(j) & =f_{k-1}^{m}(j-\binom{m}{k})+2^m & \text{as} \; \binom{m}{k} <j \leq \binom{m+1}{k} \end{align*} $$

   By the claim $c_k^{m}(f_k^m(i))$ holds, which by definition we get $|f_k^m(i)| \leq m$ . We have,

   $$\begin{align*}|f_{k}^{m}(i)| = |f_{k-1}^{m}(j-\binom{m}{k})+2^m|. \end{align*}$$

   However, $|f_{k}^{m}(i)| \leq m$ , which is a contradiction with

   $$\begin{align*}|f_{k-1}^{m}(j-\binom{m}{k})+2^m|> m.\\[-42pt] \end{align*}$$