AKS (#7)

* First version for AKS

* Fix `R` upper bound

* Add theorem explaining why some theorems about concavity are needed for estimations

* Fix log to wrong base

* Split the different claims for 6.1, formatting.

* Add part for claim 3

* Fix escape sequence

* Fixed description of E in cl3

* Update dependencies in aks61c3.md

---------

Co-authored-by: metakunt <[email protected]>

AKS (PRIMES is in P)/README.md

@@ -0,0 +1,12 @@
+## PRIMES IS IN P ##
+
+The **AKS primality test** (also known as *Agrawal–Kayal–Saxena primality test* and *cyclotomic AKS test*) is a deterministic primality-proving algorithm created and published by Manindra Agrawal, Neeraj Kayal, and Nitin Saxena, computer scientists at the Indian Institute of Technology Kanpur, on August 6, 2002, in an article titled [PRIMES is in P](http://www.cse.iitk.ac.in/users/manindra/algebra/primality_v6.pdf).
+
+The AKS primality test is based upon the following theorem: 
+
+Given an integer $n \geq 2$ and integer $a$ coprime to $n$, $n$ is prime if and only if the polynomial congruence relation
+
+  $$(X+a)^{n}\equiv X^{n}+a{\pmod {n}}$$
+
+holds within the polynomial ring $(\mathbb{Z}/n\mathbb{Z})[X]$.
+

AKS (PRIMES is in P)/aks10kbnd.md

@@ -0,0 +1,22 @@
++++
+reference = "Lemma 2.3 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
+statement = """
+$e |- 
+$e |- ( ph -> N e. RR ) $.
+$e |- ( ph -> 10000 <_ N ) $.
+$p |- ( ph -> ( ( 2 logb N ) ^ ( 7 / 2 ) ) < N ) $.
+"""
+dependencies = ["taylconcavebnd"]
++++
+Use Taylor's expansion for $f(x) = (log_2(x))^{\frac{7}{2}}$ at $x = 10000$.
+Then observe that $f^{\prime\prime}(x) < 0$, $f^{\prime}(x)<1$ and $f(x) < 10000$ for 
+$x\geq 10000$.
+
+This suffices, as $f(x)\leq f(10000)+(x-10000)f^{\prime}(x)$
+
+$\leq 10000 + ( x-10000)f^{\prime}(10000)$
+
+$\leq10000+(x-10000)$
+
+$\leq x$

AKS (PRIMES is in P)/aks22.md

@@ -0,0 +1,19 @@
++++
+reference = "Theorem 2.2 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
+statement = """
+$e |- 
+$e |- ( ph -> N e. ( ZZ>= ` 2 ) ) $.
+$e |- ( ph -> R e. ( 1 ... ( |^ ` ( ( 2 log N ) ^ 5 ) ) ) ) $.
+$e |- ( ph -> A e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi ` R )  ) x. ( 2 log N )  )  ) ) ) $.
+$e |- ( ph -> ( A gcd N ) = 1 ) $.
+$e |- ( ph ->  = 1 ) $.
+$p |- ( ph -> E. m e. NN ( P ^ m ) = N ) $.
+"""
+dependencies = ["odrlblem","rhmextex","aks61"]
++++
+Consider some $n\geq 2$. For all $1 \leq r \leq \left\lceil log_5 n \right\rceil$ and $1 \leq a \leq \left\lfloor \sqrt{ \phi(r)} log n \right\lfloor$, assume that the following hold:
+* gcd(a, n) = 1, and
+* In $(\mathbb{Z}/n)[x]/(x^r − 1)$, we have $(x + a)^n \equiv x^n + a$.
+
+Then $n$ is a power of a prime.

AKS (PRIMES is in P)/aks61.md

@@ -0,0 +1,26 @@
++++
+reference = "Theorem 6.1 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
+statement = """
+aks.1 $e |- G = ( Z/nZ ` R ) $.
+aks.2 $e |- O = ( od ` G ) $.
+aks.3 $e |- F = ( GF_oo ` P ) $. // F is the algebraic closure of F_p
+aks.4 $e |- A = ( ( ZRHom ` P ) ` a ) $. // ` A ` is the image of a by the canonical homomorphism from the integers to the ring ` F `
+aks.5 $e |- .^ = ( .g ` ( mulGrp ` F ) ) $.
+aks.6 $e |- .1. = ( 1r ` F ) $.
+aks.7 $e |- +. = ( +g ` F ) $.
+aks.8 $e |- .0. = ( 0g ` F ) $.
+aks.9 $e |- ( ph -> N e. ( ZZ>= ` 2 ) ) $.
+aks.10 $e |- ( ph -> P e. Prime ) $.
+aks.11 $e |- ( ph -> P || N ) $.
+aks.12 $e |- ( ph -> R e. ( ZZ>= ` 2 ) ) $.
+aks.13 $e |- ( ph -> ( N gcd R ) = 1 ) $.
+aks.14 $e |- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( O ` N ) ) $.
+aks.15 $e |- ( ph -> M e. F ) // M is an element of the splitting field
+aks.16 $e |- ( ph -> ( R .^ M ) = .1. ) $. // also state that R is minimal so that it is a primitive root?
+aks.17 $e |- ( ( ph /\\ a e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) ) -> ( a gcd N ) = 1 ) $.
+aks.18 $e |- ( ( ph /\\ a e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) ) -> ( N .^ ( M .+ A ) ) = ( ( N .^ M ) .+ A ) ) $.
+aks $p |- ( ph -> E. m e. NN ( P ^ m ) = N ) $= ? $. // AKS Result, if 1-18 hold, then N is a power of P.
+"""
+dependencies = ["aks61c2","aks61c7"]
++++

AKS (PRIMES is in P)/aks61c1.md

@@ -0,0 +1,4 @@
++++
+reference = "Claim 1 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
++++

AKS (PRIMES is in P)/aks61c2.md

@@ -0,0 +1,5 @@
++++
+reference = "Claim 2 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
+dependencies = ["aks61c1"]
++++

AKS (PRIMES is in P)/aks61c3.md

@@ -0,0 +1,5 @@
++++
+reference = "Claim 3 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
+dependencies = ["cl3"]
++++

AKS (PRIMES is in P)/aks61c4.md

@@ -0,0 +1,5 @@
++++
+reference = "Claim 4 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
+dependencies = []
++++

AKS (PRIMES is in P)/aks61c5.md

@@ -0,0 +1,4 @@
++++
+reference = "Claim 5 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
++++

AKS (PRIMES is in P)/aks61c6.md

@@ -0,0 +1,5 @@
++++
+reference = "Claim 6 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
+dependencies = ["aks61c5"]
++++

AKS (PRIMES is in P)/aks61c7.md

@@ -0,0 +1,5 @@
++++
+reference = "Claim 2 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
+dependencies = ["aks61c3","aks61c4","aks61c6"]
++++

AKS (PRIMES is in P)/akslb.md

@@ -0,0 +1,12 @@
++++
+reference = "Lemma 2.3 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
+statement = """
+$e |- ( ph -> N e. ( ZZ>= ` ; ; ; ; 1 0 0 0 0 ) ) $.
+$e |- ( ph -> R e. ( 1 ... ( |^ ` ( ( 2 log N ) ^ 5 ) ) ) ) $.
+$e |- ( ph -> A e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi ` R )  ) x. ( 2 log N )  )  ) ) ) $.
+$p |- ( ph -> A < N ) $.
+"""
+dependencies = ["phibnd","aks10kbnd"]
++++
+Eliminate lower values of $n$: the hypotheses of Theorem 2.2 only need to be checked for fairly large $n$.

AKS (PRIMES is in P)/aksth.md

@@ -0,0 +1,10 @@
++++
+reference = "https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
+dependencies = ["aksthr","aks22","akslb"]
++++
+Given an integer $n\geq 2$ and integer $a$ coprime to $n$, $n$ is prime if and only if the polynomial congruence relation
+$$(X+a)^{n}\equiv X^{n}+a{\pmod {n}}$$
+holds within the polynomial ring $(\mathbb{Z}/n\mathbb{Z})[X]$.
+
+It is sufficient to evaluate that equality in a polynomial ring $(\mathbb{Z}/r\mathbb{Z})[X]$, and the number of $a$'s to test and the appropriate $r$ are both bounded by a polynomial in $log n$ and therefore, there is a deterministic polynomial time algorithm for testing primality.

AKS (PRIMES is in P)/aksthr.md

@@ -0,0 +1,6 @@
++++
+reference = "Lemma 2.1 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
+dependencies = ["prmfac1", "dvdsfac"]
++++
+Simpler direction of the AKS theorem: 

AKS (PRIMES is in P)/cl3.md

@@ -0,0 +1,34 @@
++++
+reference = "Part for Claim 3 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Draft"
+statement = """
+cl3a.1 $e |- G = ( Z/nZ ` R ) $.
+cl3a.2 $e |- O = ( od ` G ) $.
+cl3a.3 $e |- F = ( GF_oo ` P ) $. // F is the algebraic closure of F_p
+cl3a.4 $e |- A = ( ( ZRHom ` P ) ` a ) $. // ` A ` is the image of a by the canonical homomorphism from the integers to the ring ` F `
+cl3a.5 $e |- .^ = ( .g ` ( mulGrp ` F ) ) $.
+cl3a.6 $e |- .1. = ( 1r ` F ) $.
+cl3a.7 $e |- +. = ( +g ` F ) $.
+cl3a.8 $e |- .0. = ( 0g ` F ) $.
+cl3a.9 $e |- ( ph -> N e. ( ZZ>= ` 2 ) ) $.
+cl3a.10 $e |- ( ph -> P e. Prime ) $.
+cl3a.11 $e |- ( ph -> P || N ) $.
+cl3a.12 $e |- ( ph -> R e. ( ZZ>= ` 2 ) ) $.
+cl3a.13 $e |- ( ph -> ( N gcd R ) = 1 ) $.
+cl3a.14 $e |- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( O ` N ) ) $.
+cl3a.15 $e |- ( E = ran ( k e. NN0 , j e. NN0 |-> ( ( ( N / P ) ^ k ) x. ( P ^ j ) ) ) )  $.
+cl3a.16 $e |- ( M = ( ZRHom ` G ) ) $. //I think we need to define a map as in preparation for claim 3.
+cl3a $e |- ( ph ->  ( M " E ) = ( Base ` G ) )
+"""
+dependencies = ["znzrhfo","cl3contnpows"]
++++
+
+This is a necessary step for claim 3, essentially we want to show that
+the restriction of the homomorphism of E -> Z/rZ is surjective.
+This allows us to reason that the image contains r elements.
+Assume it is not true, then there is an element in Z/rZ that is not hit by the homomorphism,
+but this is a contradiction by our result. Thus we can replace ord_r(n) with barE
+but by cl3a.14 claim 3 follows.
+
+We also need to show that all powers of n are in E, but this should be trivial.
+This should be proven in cl3contnpows.

AKS (PRIMES is in P)/lcmineqlem.md

@@ -0,0 +1,10 @@
++++
+reference = "Theorem 3.1 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "Formalized"
+statement = """
+    lcmineqlem.1 $e |- ( ph -> N e. NN ) $.
+    lcmineqlem.2 $e |- ( ph -> 7 <_ N ) $.
+    lcmineqlem $p |- ( ph -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) $.
+"""
++++
+The least common multiple inequality lemma, a central result for future use.  

AKS (PRIMES is in P)/odrlblem.md

@@ -0,0 +1,14 @@
++++
+reference = "Theorem 4.1 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf"
+state = "ReadyForStmt"
+statement = """
+$e |- G = ( Z/nZ ` r ) $.
+$e |- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) $.
+$p |- ( N e. ( ZZ>= ` 3 ) -> E. r e. ( 1 ... B ) ( ( r gcd N ) = 1 /\\ ( 2 logb N ) < ( od ` G ) ) ) $.
+"""
+dependencies = ["lcmineqlem", "3lexlogpow5ineq3"]
++++
+### Making $n$ have high order modulo $r$.
+
+For $n \geq 3$, there exists some $r \leq \left\lceil log_5 n \right\rceil$ such that $gcd(n, r) = 1$ and $od_r(n) > log_2 n$.
+

AKS (PRIMES is in P)/rhmextex.md

@@ -0,0 +1,6 @@
++++
+
++++
+### Extension of ring homomorphism over ring extensions
+Let $A \subset B$ be a finite ring extension. Fix a ring homomorphism $F : A → C$, where $C$ is an algebraically closed field. 
+There is a ring homomorphisms $\overline{F}: B → C$ that extends $F$.

AKS (PRIMES is in P)/taylconcavebnd.md

@@ -0,0 +1,2 @@
++++
++++