Finish proof of aks (#4979)

* finish proof of aks

* typo

* suggestions

Author: metakunt

set.mm

@@ -692967,6 +692967,51 @@ fixed reference functional determined by this vector (corresponding to
       GQVNVKVACOVNVIURVJUTVNVHUQUOVGBUPKUGRVGBUSUHUASUIVMHUFTACGHUJUKEULFUL $.
   $}
 
+  ${
+    $d A a $.  $d N a k q $.  $d N k n p q $.  $d R a k $.  $d R k n p $.
+    $d a k ph q $.  $d n p ph q $.
+    aks5.1 $e |- A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x.
+     ( 2 logb N ) ) ) $.
+    aks5.2 $e |- X = ( var1 ` ( Z/nZ ` N ) ) $.
+    aks5.3 $e |- S = ( Poly1 ` ( Z/nZ ` N ) ) $.
+    aks5.4 $e |- L = ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) )
+      X ) ( -g ` S ) ( 1r ` S ) ) } ) $.
+    aks5.5 $e |- ( ph -> N e. ( ZZ>= ` 3 ) ) $.
+    aks5.6 $e |- ( ph -> R e. NN ) $.
+    aks5.7 $e |- ( ph -> ( N gcd R ) = 1 ) $.
+    aks5.8 $e |- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) ) $.
+    aks5.9 $e |- ( ph -> A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp `
+    S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ]
+      ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S )
+       ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) $.
+    aks5.10 $e |- ( ph -> A. a e. ( 1 ... A ) ( a gcd N ) = 1 ) $.
+    $( The AKS Primality test, given an integer ` N ` greater than or equal to
+       3, find a coprime ` R ` such that ` R ` is big enough.  Then, if a bunch
+       of polynomial equalities in the residue ring hold then ` N ` is a prime
+       power.  Currently depends on the axiom ~ ax-exfinfld , since we
+       currently do not have the existence of finite fields in the database.
+       (Contributed by metakunt, 16-Aug-2025.) $)
+    aks5 $p |- ( ph -> E. p e. Prime E. n e. NN N = ( p ^ n ) ) $=
+      ( vq vk cv cdvds wbr cexp co wceq cn wrex cprime wcel cbs chash codz cchr
+      wa cfv cfield simprl simplr ad2antrr prmnn syl cz cgcd c1 nnzd gcdcomd c3
+      w3a cuz eluzelz 3jca eqtrd simpr jca rpdvds syl2anc odzcl nnnn0d nnexpcld
+      syl3anc eqeltrd eqid simprr ad4antr simpllr eqbrtrd clogb clt cmin eqcomd
+      odzid oveq1d breqtrd czrh cplusg cmgp cmg cqg cec wral aks5lem8 exfinfldd
+      c2 cfz r19.29a uzuzle23 exprmfct ) AUAUCZGUDUEZGIUCEUCUFUGUHEUIUJIUKUJZUA
+      UKAXKUKULZUQZXLUQZUBUCZUMURUNURZXKXKCUOURZURZUFUGZUHZXQUPURZXKUHZUQZXMUBU
+      SXPXQUSULZUQZYEUQZBYCCDEXQFGHIJJYHXRYAUIYGYBYDUTZYHXKXTYHXNXKUIULZXPXNYFY
+      EAXNXLVAZVBZXKVCZVDZYHXTXPXTUIULZYFYEXPCUIULZXKVEULZXKCVFUGZVGUHZYOAYPXNX
+      LPVBZXPXKXPXNYJYKYMVDVHZXPYRCXKVFUGZVGXPXKCUUAXPCYTVHZVIXPCVEULZYQGVEULZV
+      KCGVFUGZVGUHZXLUQUUBVGUHXPUUDYQUUEUUCUUAXPGVJVLURULZUUEAUUHXNXLOVBVJGVMVD
+      ZVNXPUUGXLXPUUFGCVFUGZVGXPCGUUCUUIVIAUUJVGUHZXNXLQVBVOXOXLVPVQCXKGVRVSVOZ
+      XKCVTWCZVBWAWBWDYCWEXPYFYEVAYHYCXKUKYGYBYDWFZYLWDAYPXNXLYFYEPWGZAUUHXNXLY
+      FYEOWGYHYCXKGUDUUNXOXLYFYEWHWIAUUKXNXLYFYEQWGKAXFGWJUGXFUFUGGXSURWKUEXNXL
+      YFYERWGYHCYAVGWLUGZXRVGWLUGUDYHYPYQYSCUUPUDUEUUOYHXKYNVHXPYSYFYEUULVBXKCW
+      NWCYHYAXRVGWLYHXRYAYIWMWOWPAGHJUCZDWQURURZDWRURZUGDWSURWTURZUGDFXAUGZXBGH
+      UUTUGUURUUSUGUVAXBUHJVGBXGUGZXCXNXLYFYESWGAUUQGVFUGVGUHJUVBXCXNXLYFYETWGM
+      NLXDXPXKUBXTYKUUMXEXHAGXFVLURULZXLUAUKUJAUUHUVCOGXIVDGUAXJVDXH $.
+  $}
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Permutation results