proposition: Lemma cyclotomic_special_order k p : (prime p -> 0 < k -> 1 < order_modn k p -> exists h : {poly 'F_p}, [/\ monic_irreducible_poly h, (h %| 'X^k - 1)%R, size h = (order_modn k p).+1 & poly_order h 'X k = k] )%N.
proof: Proof. set d := order_modn _ _. move=> pP k_gt0 d_gt1. have p_gt1 := prime_gt1 pP. have k_gt1 := order_modn_gt1 d_gt1. have kCp := order_modn_coprime d_gt1. have d_gt0 : 0 < d by apply: leq_trans d_gt1. have /= [L LC] := Fp_splittingField pP d_gt0. set m := p ^ d in LC. have m_gt1: m > 1 by rewrite (ltn_exp2l 0) ?prime_gt1. have m_gt0 := ltnW m_gt1; have m1_gt0: m.-1 > 0 by rewrite -ltnS prednK. pose Fm := FinFieldExtType L. have /hasP[x _ xE] : has (m.-1).-primitive_root [seq val i | i <- enum (Finite.clone _ {unit Fm})]. apply: cyclic.has_prim_root => //. - apply/allP => i /mapP[/= x _ -> /=]. apply/unity_rootP => /=. rewrite -FinRing.val_unitX -(_ : #|[set : {unit Fm}]%g| = m.-1). by rewrite cyclic.expg_cardG ?inE. by rewrite card_finField_unit LC. - rewrite map_inj_uniq; first by apply: enum_uniq. by apply: val_inj. by rewrite size_map -cardE -cardsT card_finField_unit LC. have kDm1 : (k %| m.-1)%N by rewrite -subn1 -eqn_mod_dvd // order_modn_exp. have mkDm1 : (m.-1 %/ k %| m.-1)%N. by apply/dvdnP; exists k; rewrite mulnC divnK. pose z := x ^+ (m.-1 %/ k). have kPr : k.-primitive_root z. rewrite {1}(_ : k = m.-1 %/ gcdn (m.-1 %/ k) m.-1)%N //. by apply: exp_prim_root. by rewrite (gcdn_idPl mkDm1) divnA // mulnC mulnK. have /polyOver1P[h hE] := minPolyOver 1 z. have g1L : galois 1%AS {: L}%AS. by apply: finField_galois (sub1v _). pose g := ('Gal({: L}%AS /<<1; z>>))%G. pose E := <<1; z>>%VS. pose e := \dim E. have dE : d = \dim {: L}. have /eqP := @card_vspace _ Fm _ {:L}. by rewrite card_vspacef LC card_Fp // eqn_exp2l // => /eqP. have eDd : (e %| d)%N. by rewrite dE; apply/field_dimS/subvf. have kDpe : (k %| (p ^ e).-1)%N. rewrite (prim_order_dvd kPr) -subn1 expfB ?expr1; last first. by rewrite -(exp1n e) ltn_exp2r ?prime_gt1 // adim_gt0. have: z \in E by apply: memv_adjoin. rewrite Fermat's_little_theorem -/E card_Fp -/e // => /eqP->. rewrite divff //. apply/eqP=> zE0; have /eqP := prim_expr_order kPr. by rewrite zE0 expr0n eqn0Ngt k_gt0 eq_sym oner_eq0. have peE1 : p ^ e = 1 %[mod k]. rewrite -[_ ^ _]prednK ?expn_gt0 ?prime_gt0 //. by rewrite -addn1 -modnDm (eqP kDpe) add0n modn_mod. have hS : size h = d.+1. have := size_minPoly 1%AS z. rewrite /adjoin_degree dimv1 divn1 -/E -/e. rewrite hE size_map_poly prednK ?adim_gt0 // => ->. congr (_.+1); apply/eqP; rewrite eqn_dvd. apply/andP; split. by rewrite dE; apply/field_dimS/subvf. rewrite /d order_modnE //; case: insubP => [u|/negP[]]; rewrite !unitZpE //=. move=> _ uE. rewrite cyclic.order_dvdn. apply/eqP/val_eqP. rewrite FinRing.val_unitX /= uE. rewrite -natrX. by rewrite -(Zp_nat_mod k_gt1) peE1 modn_small //. have minD : minPoly 1%AS z %| 'X^k - 1. apply: minPoly_dvdp. Time by rewrite !rpredB //= ?rpredX //= ?polyOverX //= ?rpred1 //=. rewrite rootE !hornerE -exprM divnK //. by rewrite prim_expr_order // subrr. have hD : h %| 'X^k - 1. move: minD. have ->: 'X^k - 1 = map_poly (in_alg L) ('X^k - 1). by rewrite raddfB /= rmorphXn /= map_polyX /= rmorph1. by rewrite hE dvdp_map. have hM : h \is monic. have := monic_minPoly 1 z. by rewrite hE map_monic. exists h; split => //. - split => //. split=> [|p1 Sp1 p1Dh]; first by rewrite hS. pose fp1 := map_poly (in_alg L) p1. have /(minPoly_irr (alg_polyOver _ _))/orP[] : fp1 %| minPoly 1%AS z by rewrite hE dvdp_map. by rewrite hE eqp_map. rewrite -(_ : map_poly (in_alg L) 1 = 1). by rewrite eqp_map -size_poly_eq1 (negPf Sp1). by rewrite map_polyC /= scale1r. apply: poly_orderE=> [||k1 k1_gt0 /eqP]; first by rewrite k_gt0 leqnn. apply/eqP; rewrite -[1](@rmodp_small _ _ h) ?size_poly1 ?hS //. rewrite -subr_eq0 -rmodpB //. by rewrite -[_ == 0]/(rdvdp h ('X^k - 1)) -dvdpE. rewrite -[1](@rmodp_small _ _ h) ?size_poly1 ?hS //. rewrite -subr_eq0 -rmodpB //. rewrite -[_ == 0]/(rdvdp h ('X^k1 - 1)) -dvdpE => hDk1. apply: dvdn_leq => //. suff: minPoly 1%AS z %| 'X^k1 - 1. move=> Hk1. rewrite (prim_order_dvd kPr). have : ('X^k1 - 1).[z] == 0. by case/dvdpP: Hk1 => r ->; rewrite hornerE minPolyxx mulr0. by rewrite !hornerE subr_eq0. rewrite hE. have ->: 'X^k1 - 1 = map_poly (in_alg L) ('X^k1 - 1). by rewrite raddfB /= rmorphXn /= map_polyX /= rmorph1. by rewrite dvdp_map. Time Qed. Lemma main_aks p n k (F := (FinRing.Ring.clone _ 'F_p)) : prime p -> aks_criteria F n k -> is_power n p. Proof. move=> pP; have p_gt1 := prime_gt1 pP. have pC : p \in [char F] by apply: char_Fp. pose a := (up_log 2 n) ^ 2; pose s := (sqrtn (totient k) * up_log 2 n)%N. move => [n_gt0 k_gt0 /(_ p pC) [pO_gt1 pDn kLp lnLnO Hr]]. have k_gt1 : 1 < k by apply: order_modn_gt1 pO_gt1. have := dvdn_leq n_gt0 pDn. rewrite leq_eqVlt => /orP[/eqP<-|pLn]; first by rewrite is_power_id. have [/eqP nE|/negP nis2p] := boolP (is_2power n). move: pDn; rewrite nE. rewrite Euclid_dvdX // => /andP[/prime_nt_dvdP->] //. by move=> _; apply: is_power_exp. by case: (p) pP => // [] // []. have n_gt1 : 1 < n. apply: leq_trans (prime_gt1 pP) _. by apply: dvdn_leq. have n_gt2 : 2 < n by case: (n) n_gt1 nis2p => [|[|[|]]]. have kCn : coprime k n. apply: order_modn_coprime. apply: leq_trans lnLnO. rewrite (@ltn_exp2r 1 _ 2) //. by apply: (@leq_up_log 2 3). have kCp : coprime k p by apply: order_modn_coprime. have nI : is_iexp (GRing.Ring.clone _ 'F_p) k s n. split => [|c cB]; first by rewrite coprime_sym. apply/eqP. rewrite comp_polyD comp_polyC comp_polyX. by apply: Hr. have [h [hMI hDxk1 jS hO]]:= cyclotomic_special_order pP k_gt0 pO_gt1. have [//|/negP nP] := boolP (is_power n p). have /classicP[] := @Mk_Cexists F k s. move=> [M hMk]. have /classicP[] := @Qh_Cexists F k s h. move=> [Q hQh]. pose t := #|M|. have t_gt1 : 1 < t. apply: leq_trans pO_gt1 _. apply: is_iexpm_order (hMk) _ => //. apply: is_iexp_fin_char; first by apply: char_Fp. by rewrite coprime_sym. have nLst : n ^ sqrtn t < 2 ^ minn s t. apply: exp_Mk_upper_bound hMk _ _ _ _ _ _ _ _ => //. by apply/negP. have stLQ : 2 ^ minn s t <= #|Q|. apply: (@lower_bound_card_Qh _ _ _ _ p) => //; first by rewrite -dvdpE. rewrite muln_gt0 sqrtn_gt0 totient_gt0 k_gt0. rewrite (@leq_up_log 2 2) //=. apply: leq_trans (kLp). rewrite ltnS. apply: leq_trans (totient_leq _). have /andP[/(leq_trans _)->//] := sqrtn_bound (totient k). rewrite expnS expn1 leq_mul2l -(sqrnK (up_log 2 n)). rewrite leq_sqrtn ?orbT //. by apply: leq_trans (leq_order_totient n _). pose q := (n %/ p)%N. have nE : n = (q * p)%N. by rewrite [n](divn_eq _ p) (eqP pDn) addn0. have q_gt1 : 1 < q. case: leqP => //. move: n_gt1 nP; rewrite nE. by case: (q) => [|[|]] // _ []; rewrite mul1n is_power_id. have pI : is_iexp F k s p by apply: is_iexp_fin_char; rewrite 1? coprime_sym. have qI : is_iexp F k s q by apply: is_iexp_fin_div; rewrite 1? coprime_sym. pose N1 := Nbar p q (sqrtn t). pose f := fun i : 'I_((p * q) ^ sqrtn t).+1 => inZp i : 'Z_k. have : #|f @: N1| <= t. apply/subset_leq_card/subsetP => x /imsetP[y /imsetP[/= [i1 j1 _]-> -> /=]]. set m := (_ ^ _ * _)%N. have mI : is_iexp F k s m. by apply: is_iexp_mul; apply: is_iexp_X. case: hMk => //= /(_ _ mI)/eqP[]. rewrite /= Zp_cast // [(m %% _)%N]modn_small //. by rewrite ltnS expnMn leq_mul // leq_exp2l // -ltnS. rewrite leqNgt=> /negP[]. rewrite card_in_imset; last first. apply: (is_iexp_inj hMk hQh) => //; first by rewrite -dvdpE. rewrite mulnC -nE. by apply: leq_trans stLQ. rewrite card_Nbar //; last first. move=> H; case: nP. by rewrite nE (eqP H) -expnSr is_power_exp. by have /andP[] := sqrtn_bound t. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound