Hi, Yes, I think what you need for aks-16-18 is something like:
aks.16 $e |- ph -> A. a e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) ) ( ( a gcd N ) = 1 /\ ( ( M + a ) ^ N ) = ( ( M ^ N ) + a ) ) $. Or equivalently: aks.16ALT $e |- ( ( ph /\ a e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) ) -> ( a gcd N ) = 1 ) $. aks.17ALT $e |- ( ( ph /\ a e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) ) -> ( ( M + a ) ^ N ) = ( ( M ^ N ) + a ) ) $. Using a set variable `a` there will allow you to switch easily to the universal quantifier. For aks.7, you'll want to have G = ( Z/nZ ` N ), and then G is your group (or actually, ring). For aks,11 and aks.14, you can probably keep R in NN0, and use ( ( ZRHom ` G ) ` R ) to map it to the corresponding element of G = ( Z/nZ ` N ) (which is actually an equivalence class). As far as the Galois Limit Field GF_oo is concerned, there are not theorems about it yet, so my guess is that we'll need to develop that theory first! _ Thierry On 24/05/2024 15:21, 'asdf asdf' via Metamath wrote:
Hey guys, I have set up a working group to prove theorem 6.1 of https://www3.nd.edu/~andyp/notes/AKS.pdf Short background, AKS is the first /general/, /polynomial-time/, /deterministic/, and /unconditionally correct/ primality algorithm. It is unconditionally correct because it doesn't depend on the generalized Riemann hypothesis. It is general because it works for all numbers and not just for Mersenne Numbers for example. I have tried to formalize the hypotheses that need to hold. One typically shows that for all A as in aks.16: aks.17 and aks.18 hold. Therefore N is a prime power, then you just check that the exponent must be 1 and you have proven N to be a prime. aks.1 $e |- ( ph -> N e. NN ) $. aks.2 $e |- ( ph -> 2 <_ N ) $. aks.3 $e |- ( ph -> P e. Prime ) $. aks.4 $e |- ( ph -> R e. NN ) $. aks.5 $e |- ( ph -> 2 <_ R ) $. aks.6 $e |- ( ph -> ( N gcd R ) = 1 ) $. aks.7 $e |- ( Z/nZ ` N ) = ( Base ` G ) $. aks.8 $e |- O = ( od ` G ) $. aks.9 $e |- +. = ( +g ` G ) $. aks.10 $e |- .0. = ( 0g ` G ) $. aks.11 $e |- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( O ` R ) ) $. // TODO R needs to be in Z\nZ aks.12 $e |- F = ( GF_oo ` P ) $. //This is the algebraic closure of F_p aks.13 $e |- ( ph -> M e. F ) // M is an element of the splitting field aks.14 $e |- ( ph -> ( M ^ R ) = 1 ) $. //todo replace ^, R and 1 with their respective GF equivalent, and also state that R is minimal so that it is a primitive root. aks.15 $e |- ( E = ( .g ` F ) ) $. //E is the group multiplicator for GF_oo, I don't know I am entering voodoo land. aks.16 $e |- ( ph -> A e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) ) $. aks.17 $e |- ( ph -> ( A gcd N ) = 1 ) $. aks.18 $e |- ( ph -> ( ( M + A ) ^ N ) = ( ( M ^ N ) + A ) ) $. //This needs to be done in the polynomial ring over GF_oo aks $p |- ( ph -> E. m e. NN ( P ^ m ) = N ) $= ? $. // AKS Result, if 1-18 hold, then N is a power of P. aks.14 shows that mu is a r-th root. We need another condition that it is a primitive root. I have seen that Mario has defined something https://us.metamath.org/mpeuni/df-gfoo.html however there are no results associated with his definition yet. We would definitely need that it is a field, that the Frobenius is an element of it, and by the properties of the field that the inverse is also an element of it. This is very advanced for me and as such I might need some guidance where to start. One good point would be to start at GF_oo as this seems necessary for the theorem, a second good point would be to formalize the hypotheses first. I am also not sure if aks.16-18 are correct. Maybe something like this makes more sense aks.16ALT $e |- ( ( ph /\ A e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) ) -> ( A gcd N ) = 1 ) $. aks.17ALT $e |- ( ( ph /\ A e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) ) -> ( ( M + A ) ^ N ) = ( ( M ^ N ) + A ) ) $. Any feedback is welcome. ------------------------------------------------------------------------ Your E-Mail. Your Cloud. Your Office. *eclipso Mail Europe <https://www.eclipso.eu>*. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/834460ada90a2c25d144a5a9f37fbd32%40mail.eclipso.de <https://groups.google.com/d/msgid/metamath/834460ada90a2c25d144a5a9f37fbd32%40mail.eclipso.de?utm_medium=email&utm_source=footer>.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9ab6d145-6a38-49a5-883f-f12b140cfc6a%40gmx.net.
