Feasibility of Primality in Bounded Arithmetic
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914452408893440 |
|---|---|
| author | Jalali, Raheleh Ježil, Ondřej |
| author_facet | Jalali, Raheleh Ježil, Ondřej |
| contents | We prove the correctness of the AKS algorithm \cite{AKS} within the bounded arithmetic theory $T^{count}_2$ or, equivalently, the first-order consequences of the theory $VTC^0$ expanded by the smash function, which we denote by $VTC^0_2$. Our approach initially demonstrates the correctness within the theory $S^1_2 + iWPHP$ augmented by two algebraic axioms and then show that they are provable in $VTC^0_2$. The two axioms are: a generalized version of Fermat's Little Theorem and an axiom adding a new function symbol which injectively maps roots of polynomials over a definable finite field to numbers bounded by the degree of the given polynomial. To obtain our main result, we also give new formalizations of parts of number theory and algebra:
$\bullet$ In $PV_1$: We formalize Legendre's Formula on the prime factorization of $n!$, key properties of the Combinatorial Number System and the existence of cyclotomic polynomials over the finite fields $\mathbb{Z}/p$.
$\bullet$ In $S^1_2$: We prove the inequality $lcm(1,\dots, 2n) \geq 2^n$.
$\bullet$ In $VTC^0$: We verify the correctness of the Kung--Sieveking algorithm for polynomial division. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_17041 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Feasibility of Primality in Bounded Arithmetic Jalali, Raheleh Ježil, Ondřej Logic Computational Complexity We prove the correctness of the AKS algorithm \cite{AKS} within the bounded arithmetic theory $T^{count}_2$ or, equivalently, the first-order consequences of the theory $VTC^0$ expanded by the smash function, which we denote by $VTC^0_2$. Our approach initially demonstrates the correctness within the theory $S^1_2 + iWPHP$ augmented by two algebraic axioms and then show that they are provable in $VTC^0_2$. The two axioms are: a generalized version of Fermat's Little Theorem and an axiom adding a new function symbol which injectively maps roots of polynomials over a definable finite field to numbers bounded by the degree of the given polynomial. To obtain our main result, we also give new formalizations of parts of number theory and algebra: $\bullet$ In $PV_1$: We formalize Legendre's Formula on the prime factorization of $n!$, key properties of the Combinatorial Number System and the existence of cyclotomic polynomials over the finite fields $\mathbb{Z}/p$. $\bullet$ In $S^1_2$: We prove the inequality $lcm(1,\dots, 2n) \geq 2^n$. $\bullet$ In $VTC^0$: We verify the correctness of the Kung--Sieveking algorithm for polynomial division. |
| title | Feasibility of Primality in Bounded Arithmetic |
| topic | Logic Computational Complexity |
| url | https://arxiv.org/abs/2504.17041 |