src/HOL/Number_Theory/Residue_Primitive_Roots.thy
 changeset 69785 9e326f6f8a24
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Number_Theory/Residue_Primitive_Roots.thy	Mon Feb 04 12:16:03 2019 +0100
1.3 @@ -0,0 +1,1152 @@
1.4 +(*
1.5 +  File:      HOL/Number_Theory/Residue_Primitive_Roots.thy
1.6 +  Author:    Manuel Eberl
1.7 +
1.8 +  Primitive roots in residue rings: Definition and existence criteria
1.9 +*)
1.10 +section \<open>Primitive roots in residue rings and Carmichael's function\<close>
1.11 +theory Residue_Primitive_Roots
1.12 +  imports Pocklington
1.13 +begin
1.14 +
1.15 +text \<open>
1.16 +  This theory develops the notions of primitive roots (generators) in residue rings. It also
1.17 +  provides a definition and all the basic properties of Carmichael's function $\lambda(n)$, which
1.18 +  is strongly related to this. The proofs mostly follow Apostol's presentation
1.19 +\<close>
1.20 +
1.21 +subsection \<open>Primitive roots in residue rings\<close>
1.22 +
1.23 +text \<open>
1.24 +  A primitive root of a residue ring modulo \<open>n\<close> is an element \<open>g\<close> that \<^emph>\<open>generates\<close> the
1.25 +  ring, i.\,e.\ such that for each \<open>x\<close> coprime to \<open>n\<close> there exists an \<open>i\<close> such that $x = g^i$.
1.26 +  A simpler definition is that \<open>g\<close> must have the same order as the cardinality of the
1.27 +  multiplicative group, which is $\varphi(n)$.
1.28 +
1.29 +  Note that for convenience, this definition does \<^emph>\<open>not\<close> demand \<open>g < n\<close>.
1.30 +\<close>
1.31 +inductive residue_primroot :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
1.32 +  "n > 0 \<Longrightarrow> coprime n g \<Longrightarrow> ord n g = totient n \<Longrightarrow> residue_primroot n g"
1.33 +
1.34 +lemma residue_primroot_def [code]:
1.35 +  "residue_primroot n x \<longleftrightarrow> n > 0 \<and> coprime n x \<and> ord n x = totient n"
1.36 +  by (simp add: residue_primroot.simps)
1.37 +
1.38 +lemma not_residue_primroot_0 [simp]: "~residue_primroot 0 x"
1.39 +  by (auto simp: residue_primroot_def)
1.40 +
1.41 +lemma residue_primroot_mod [simp]: "residue_primroot n (x mod n) = residue_primroot n x"
1.42 +  by (cases "n = 0") (simp_all add: residue_primroot_def)
1.43 +
1.44 +lemma residue_primroot_cong:
1.45 +  assumes "[x = x'] (mod n)"
1.46 +  shows   "residue_primroot n x = residue_primroot n x'"
1.47 +proof -
1.48 +  have "residue_primroot n x = residue_primroot n (x mod n)"
1.49 +    by simp
1.50 +  also have "x mod n = x' mod n"
1.51 +    using assms by (simp add: cong_def)
1.52 +  also have "residue_primroot n (x' mod n) = residue_primroot n x'"
1.53 +    by simp
1.54 +  finally show ?thesis .
1.55 +qed
1.56 +
1.57 +lemma not_residue_primroot_0_right [simp]: "residue_primroot n 0 \<longleftrightarrow> n = 1"
1.58 +  by (auto simp: residue_primroot_def)
1.59 +
1.60 +lemma residue_primroot_1_iff: "residue_primroot n (Suc 0) \<longleftrightarrow> n \<in> {1, 2}"
1.61 +proof
1.62 +  assume *: "residue_primroot n (Suc 0)"
1.63 +  with totient_gt_1[of n] have "n \<le> 2" by (cases "n \<le> 2") (auto simp: residue_primroot_def)
1.64 +  hence "n \<in> {0, 1, 2}" by auto
1.65 +  thus "n \<in> {1, 2}" using * by (auto simp: residue_primroot_def)
1.66 +qed (auto simp: residue_primroot_def)
1.67 +
1.68 +
1.69 +subsection \<open>Primitive roots modulo a prime\<close>
1.70 +
1.71 +text \<open>
1.72 +  For prime \<open>p\<close>, we now analyse the number of elements in the ring $\mathbb{Z}/p\mathbb{Z}$
1.73 +  whose order is precisely \<open>d\<close> for each \<open>d\<close>.
1.74 +\<close>
1.75 +context
1.76 +  fixes n :: nat and \<psi>
1.77 +  assumes n: "n > 1"
1.78 +  defines "\<psi> \<equiv> (\<lambda>d. card {x\<in>totatives n. ord n x = d})"
1.79 +begin
1.80 +
1.81 +lemma elements_with_ord_restrict_totatives:
1.82 +  "d > 0 \<Longrightarrow> {x\<in>{..<n}. ord n x = d} = {x\<in>totatives n. ord n x = d}"
1.83 +  using n by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I le_neq_trans)
1.84 +
1.85 +lemma prime_elements_with_ord:
1.86 +  assumes "\<psi> d \<noteq> 0" and "prime n"
1.87 +      and a: "a \<in> totatives n" "ord n a = d" "a \<noteq> 1"
1.88 +  shows   "inj_on (\<lambda>k. a ^ k mod n) {..<d}"
1.89 +    and   "{x\<in>{..<n}. [x ^ d = 1] (mod n)} = (\<lambda>k. a ^ k mod n)  {..<d}"
1.90 +    and   "bij_betw (\<lambda>k. a ^ k mod n) (totatives d) {x\<in>{..<n}. ord n x = d}"
1.91 +proof -
1.92 +  show inj: "inj_on (\<lambda>k. a ^ k mod n) {..<d}"
1.93 +    using inj_power_mod[of n a] a by (auto simp: totatives_def coprime_commute)
1.94 +  from a have "d > 0" by (auto simp: totatives_def coprime_commute)
1.95 +  moreover have "d \<noteq> 1" using a n
1.96 +    by (auto simp: ord_eq_Suc_0_iff totatives_less cong_def)
1.97 +  ultimately have d: "d > 1" by simp
1.98 +
1.99 +  have *: "(\<lambda>k. a ^ k mod n)  {..<d} = {x\<in>{..<n}. [x ^ d = 1] (mod n)}"
1.100 +  proof (rule card_seteq)
1.101 +    have "card {x\<in>{..<n}. [x ^ d = 1] (mod n)} \<le> d"
1.102 +      using assms a by (intro roots_mod_prime_bound) (auto simp: totatives_def coprime_commute)
1.103 +    also have "\<dots> = card ((\<lambda>k. a ^ k mod n)  {..<d})"
1.104 +      using inj by (subst card_image) auto
1.105 +    finally show "card {x \<in> {..<n}. [x ^ d = 1] (mod n)} \<le> \<dots>" .
1.106 +  next
1.107 +    show "(\<lambda>k. a ^ k mod n)  {..<d} \<subseteq> {x \<in> {..<n}. [x ^ d = 1] (mod n)}"
1.108 +    proof safe
1.109 +      fix k assume "k < d"
1.110 +      have "[(a ^ d) ^ k = 1 ^ k] (mod n)"
1.111 +        by (intro cong_pow) (use a in \<open>auto simp: ord_divides'\<close>)
1.112 +      thus "[(a ^ k mod n) ^ d = 1] (mod n)"
1.113 +        by (simp add: power_mult [symmetric] cong_def power_mod mult.commute)
1.114 +    qed (use \<open>prime n\<close> in \<open>auto dest: prime_gt_1_nat\<close>)
1.115 +  qed auto
1.116 +  thus "{x\<in>{..<n}. [x ^ d = 1] (mod n)} = (\<lambda>k. a ^ k mod n)  {..<d}" ..
1.117 +
1.118 +  show "bij_betw (\<lambda>k. a ^ k mod n) (totatives d) {x\<in>{..<n}. ord n x = d}"
1.119 +    unfolding bij_betw_def
1.120 +  proof (intro conjI inj_on_subset[OF inj] equalityI subsetI)
1.121 +    fix b assume "b \<in> (\<lambda>k. a ^ k mod n)  totatives d"
1.122 +    then obtain k where "b = a ^ k mod n" "k \<in> totatives d" by auto
1.123 +    thus "b \<in> {b \<in> {..<n}. ord n b = d}"
1.124 +      using n a by (simp add: ord_power totatives_def coprime_commute)
1.125 +  next
1.126 +    fix b assume "b \<in> {x \<in> {..<n}. ord n x = d}"
1.127 +    hence b: "ord n b = d" "b < n" by auto
1.128 +    with d have "coprime n b" using ord_eq_0[of n b] by auto
1.129 +    from b have "b \<in> {x\<in>{..<n}. [x ^ d = 1] (mod n)}"
1.130 +      by (auto simp: ord_divides')
1.131 +    with * obtain k where k: "k < d" "b = a ^ k mod n"
1.132 +      by blast
1.133 +    with b(2) n a d have "d div gcd k d = ord n b"
1.134 +      using \<open>coprime n b\<close> by (auto simp: ord_power)
1.135 +    also have "ord n b = d" by (simp add: b)
1.136 +    finally have "coprime k d"
1.137 +      unfolding coprime_iff_gcd_eq_1 using d a by (subst (asm) div_eq_dividend_iff) auto
1.138 +    with k b d have "k \<in> totatives d" by (auto simp: totatives_def intro!: Nat.gr0I)
1.139 +    with k show "b \<in> (\<lambda>k. a ^ k mod n)  totatives d" by blast
1.140 +  qed (use d n in \<open>auto simp: totatives_less\<close>)
1.141 +qed
1.142 +
1.143 +lemma prime_card_elements_with_ord:
1.144 +  assumes "\<psi> d \<noteq> 0" and "prime n"
1.145 +  shows   "\<psi> d = totient d"
1.146 +proof (cases "d = 1")
1.147 +  case True
1.148 +  have "\<psi> 1 = 1"
1.149 +    using elements_with_ord_1[of n] n by (simp add: \<psi>_def)
1.150 +  thus ?thesis using True by simp
1.151 +next
1.152 +  case False
1.153 +  from assms obtain a where a: "a \<in> totatives n" "ord n a = d"
1.154 +    by (auto simp: \<psi>_def)
1.155 +  from a have "d > 0" by (auto intro!: Nat.gr0I simp: ord_eq_0 totatives_def coprime_commute)
1.156 +  from a and False have "a \<noteq> 1" by auto
1.157 +  from bij_betw_same_card[OF prime_elements_with_ord(3)[OF assms a this]] show "\<psi> d = totient d"
1.158 +    using elements_with_ord_restrict_totatives[of d] False a \<open>d > 0\<close>
1.159 +    by (simp add: \<psi>_def totient_def)
1.160 +qed
1.161 +
1.162 +lemma prime_sum_card_elements_with_ord_eq_totient:
1.163 +  "(\<Sum>d | d dvd totient n. \<psi> d) = totient n"
1.164 +proof -
1.165 +  have "totient n = card (totatives n)"
1.166 +    by (simp add: totient_def)
1.167 +  also have "totatives n = (\<Union>d\<in>{d. d dvd totient n}. {x\<in>totatives n. ord n x = d})"
1.168 +    by (force simp: order_divides_totient totatives_def coprime_commute)
1.169 +  also have "card \<dots> = (\<Sum>d | d dvd totient n. \<psi> d)"
1.170 +    unfolding \<psi>_def using n by (subst card_UN_disjoint) (auto intro!: finite_divisors_nat)
1.171 +  finally show ?thesis ..
1.172 +qed
1.173 +
1.174 +text \<open>
1.175 +  We can now show that the number of elements of order \<open>d\<close> is $\varphi(d)$ if $d\mid p - 1$
1.176 +  and 0 otherwise.
1.177 +\<close>
1.178 +theorem prime_card_elements_with_ord_eq_totient:
1.179 +  assumes "prime n"
1.180 +  shows   "\<psi> d = (if d dvd n - 1 then totient d else 0)"
1.181 +proof (cases "d dvd totient n")
1.182 +  case False
1.183 +  thus ?thesis using order_divides_totient[of n] assms
1.184 +    by (auto simp: \<psi>_def totient_prime totatives_def coprime_commute[of n])
1.185 +next
1.186 +  case True
1.187 +  have "\<psi> d = totient d"
1.188 +  proof (rule ccontr)
1.189 +    assume neq: "\<psi> d \<noteq> totient d"
1.190 +    have le: "\<psi> d \<le> totient d" if "d dvd totient n" for d
1.191 +      using prime_card_elements_with_ord[of d] assms by (cases "\<psi> d = 0") auto
1.192 +    from neq and le[of d] and True have less: "\<psi> d < totient d" by auto
1.193 +
1.194 +    have "totient n = (\<Sum>d | d dvd totient n. \<psi> d)"
1.195 +      using prime_sum_card_elements_with_ord_eq_totient ..
1.196 +    also have "\<dots> < (\<Sum>d | d dvd totient n. totient d)"
1.197 +      by (rule sum_strict_mono_ex1)
1.198 +         (use n le less assms True in \<open>auto intro!: finite_divisors_nat\<close>)
1.199 +    also have "\<dots> = totient n"
1.200 +      using totient_divisor_sum .
1.201 +    finally show False by simp
1.202 +  qed
1.203 +  with True show ?thesis using assms by (simp add: totient_prime)
1.204 +qed
1.205 +
1.206 +text \<open>
1.207 +  As a corollary, we get that the number of primitive roots modulo a prime \<open>p\<close> is
1.208 +  $\varphi(p - 1)$. Since this number is positive, we also get that there \<^emph>\<open>is\<close> at least
1.209 +  one primitive root modulo \<open>p\<close>.
1.210 +\<close>
1.211 +lemma
1.212 +  assumes "prime n"
1.213 +  shows   prime_card_primitive_roots:  "card {x\<in>totatives n. ord n x = n - 1} = totient (n - 1)"
1.214 +                                       "card {x\<in>{..<n}. ord n x = n - 1} = totient (n - 1)"
1.215 +  and     prime_primitive_root_exists: "\<exists>x. residue_primroot n x"
1.216 +proof -
1.217 +  show *: "card {x\<in>totatives n. ord n x = n - 1} = totient (n - 1)"
1.218 +    using prime_card_elements_with_ord_eq_totient[of "n - 1"] assms
1.219 +    by (auto simp: totient_prime \<psi>_def)
1.220 +  thus "card {x\<in>{..<n}. ord n x = n - 1} = totient (n - 1)"
1.221 +    using assms n elements_with_ord_restrict_totatives[of "n - 1"] by simp
1.222 +
1.223 +  note *
1.224 +  also have "totient (n - 1) > 0" using n by auto
1.225 +  finally show "\<exists>x. residue_primroot n x" using assms prime_gt_1_nat[of n]
1.226 +    by (subst (asm) card_gt_0_iff)
1.227 +       (auto simp: residue_primroot_def totient_prime totatives_def coprime_commute)
1.228 +qed
1.229 +
1.230 +end
1.231 +
1.232 +
1.233 +subsection \<open>Primitive roots modulo powers of an odd prime\<close>
1.234 +
1.235 +text \<open>
1.236 +  Any primitive root \<open>g\<close> modulo an odd prime \<open>p\<close> is also a primitive root modulo $p^k$ for all
1.237 +  $k > 0$ if $[g^{p - 1} \neq 1]\ (\text{mod}\ p^2)$. To show this, we first need the
1.238 +  following lemma.
1.239 +\<close>
1.240 +lemma residue_primroot_power_prime_power_neq_1:
1.241 +  assumes "k \<ge> 2"
1.242 +  assumes p: "prime p" "odd p" and "residue_primroot p g" and "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
1.243 +  shows   "[g ^ totient (p ^ (k - 1)) \<noteq> 1] (mod (p ^ k))"
1.244 +  using assms(1)
1.245 +proof (induction k rule: dec_induct)
1.246 +  case base
1.247 +  thus ?case using assms by (simp add: totient_prime)
1.248 +next
1.249 +  case (step k)
1.250 +  from p have "p > 2"
1.251 +    using prime_gt_1_nat[of p] by (cases "p = 2") auto
1.252 +  from assms have g: "g > 0" by (auto intro!: Nat.gr0I)
1.253 +  have "[g ^ totient (p ^ (k - 1)) = 1] (mod p ^ (k - 1))"
1.254 +    using assms by (intro euler_theorem)
1.255 +                   (auto simp: residue_primroot_def totatives_def coprime_commute)
1.256 +  from cong_to_1_nat[OF this]
1.257 +    obtain t where *: "g ^ totient (p ^ (k - 1)) - 1 = p ^ (k - 1) * t" by auto
1.258 +  have t: "g ^ totient (p ^ (k - 1)) = p ^ (k - 1) * t + 1"
1.259 +    using g by (subst * [symmetric]) auto
1.260 +
1.261 +  have "\<not>p dvd t"
1.262 +  proof
1.263 +    assume "p dvd t"
1.264 +    then obtain q where [simp]: "t = p * q" by auto
1.265 +    from t have "g ^ totient (p ^ (k - 1)) = p ^ k * q + 1"
1.266 +      using \<open>k \<ge> 2\<close> by (cases k) auto
1.267 +    hence "[g ^ totient (p ^ (k - 1)) = p ^ k * q + 1] (mod p ^ k)"
1.268 +      by simp
1.269 +    also have "[p ^ k * q + 1 = 0 * q + 1] (mod p ^ k)"
1.270 +      by (intro cong_add cong_mult) (auto simp: cong_0_iff)
1.271 +    finally have "[g ^ totient (p ^ (k - 1)) = 1] (mod p ^ k)"
1.272 +      by simp
1.273 +    with step.IH show False by contradiction
1.274 +  qed
1.275 +
1.276 +  from t have "(g ^ totient (p ^ (k - 1))) ^ p = (p ^ (k - 1) * t + 1) ^ p"
1.277 +    by (rule arg_cong)
1.278 +  also have "(g ^ totient (p ^ (k - 1))) ^ p = g ^ (p * totient (p ^ (k - 1)))"
1.279 +    by (simp add: power_mult [symmetric] mult.commute)
1.280 +  also have "p * totient (p ^ (k - 1)) = totient (p ^ k)"
1.281 +    using p \<open>k \<ge> 2\<close> by (simp add: totient_prime_power Suc_diff_Suc flip: power_Suc)
1.282 +  also have "(p ^ (k - 1) * t + 1) ^ p = (\<Sum>i\<le>p. (p choose i) * t ^ i * p ^ (i * (k - 1)))"
1.283 +    by (subst binomial) (simp_all add: mult_ac power_mult_distrib power_mult [symmetric])
1.284 +  finally have "[g ^ totient (p ^ k) = (\<Sum>i\<le>p. (p choose i) * t ^ i * p ^ (i * (k - 1)))]
1.285 +                  (mod (p ^ Suc k))" (is "[_ = ?rhs] (mod _)") by simp
1.286 +
1.287 +  also have "[?rhs = (\<Sum>i\<le>p. if i \<le> 1 then (p choose i) * t ^ i * p ^ (i * (k - 1)) else 0)]
1.288 +               (mod (p ^ Suc k))" (is "[sum ?f _ = sum ?g _] (mod _)")
1.289 +  proof (intro cong_sum)
1.290 +    fix i assume i: "i \<in> {..p}"
1.291 +    consider "i \<le> 1" | "i = 2" | "i > 2" by force
1.292 +    thus "[?f i = ?g i] (mod (p ^ Suc k))"
1.293 +    proof cases
1.294 +      assume i: "i > 2"
1.295 +      have "Suc k \<le> 3 * (k - 1)"
1.296 +        using \<open>k \<ge> 2\<close> by (simp add: algebra_simps)
1.297 +      also have "3 * (k - 1) \<le> i * (k - 1)"
1.298 +        using i by (intro mult_right_mono) auto
1.299 +      finally have "p ^ Suc k dvd ?f i"
1.300 +        by (intro dvd_mult le_imp_power_dvd)
1.301 +      thus "[?f i = ?g i] (mod (p ^ Suc k))"
1.302 +        by (simp add: cong_0_iff)
1.303 +    next
1.304 +      assume [simp]: "i = 2"
1.305 +      have "?f i = p * (p - 1) div 2 * t\<^sup>2 * p ^ (2 * (k - 1))"
1.306 +        using choose_two[of p] by simp
1.307 +      also have "p * (p - 1) div 2 = (p - 1) div 2 * p"
1.308 +        using \<open>odd p\<close> by (auto elim!: oddE)
1.309 +      also have "\<dots> * t\<^sup>2 * p ^ (2 * (k - 1)) = (p - 1) div 2 * t\<^sup>2 * (p * p ^ (2 * (k - 1)))"
1.310 +        by (simp add: algebra_simps)
1.311 +      also have "p * p ^ (2 * (k - 1)) = p ^ (2 * k - 1)"
1.312 +        using \<open>k \<ge> 2\<close> by (cases k) auto
1.313 +      also have "p ^ Suc k dvd (p - 1) div 2 * t\<^sup>2 * p ^ (2 * k - 1)"
1.314 +        using \<open>k \<ge> 2\<close> by (intro dvd_mult le_imp_power_dvd) auto
1.315 +      finally show "[?f i = ?g i] (mod (p ^ Suc k))"
1.316 +        by (simp add: cong_0_iff)
1.317 +    qed auto
1.318 +  qed
1.319 +  also have "(\<Sum>i\<le>p. ?g i) = (\<Sum>i\<le>1. ?f i)"
1.320 +    using p prime_gt_1_nat[of p] by (intro sum.mono_neutral_cong_right) auto
1.321 +  also have "\<dots> = 1 + t * p ^ k"
1.322 +    using choose_two[of p] \<open>k \<ge> 2\<close> by (cases k) simp_all
1.323 +  finally have eq: "[g ^ totient (p ^ k) = 1 + t * p ^ k] (mod p ^ Suc k)" .
1.324 +
1.325 +  have "[g ^ totient (p ^ k) \<noteq> 1] (mod p ^ Suc k)"
1.326 +  proof
1.327 +    assume "[g ^ totient (p ^ k) = 1] (mod p ^ Suc k)"
1.328 +    hence "[g ^ totient (p ^ k) - g ^ totient (p ^ k) = 1 + t * p ^ k - 1] (mod p ^ Suc k)"
1.329 +      by (intro cong_diff_nat eq) auto
1.330 +    hence "[t * p ^ k = 0] (mod p ^ Suc k)"
1.331 +      by (simp add: cong_sym_eq)
1.332 +    hence "p * p ^ k dvd t * p ^ k"
1.333 +      by (simp add: cong_0_iff)
1.334 +    hence "p dvd t" using \<open>p > 2\<close> by simp
1.335 +    with \<open>\<not>p dvd t\<close> show False by contradiction
1.336 +  qed
1.337 +  thus ?case by simp
1.338 +qed
1.339 +
1.340 +text \<open>
1.341 +  We can now show that primitive roots modulo \<open>p\<close> with the above condition are
1.342 +  indeed also primitive roots modulo $p^k$.
1.343 +\<close>
1.344 +proposition residue_primroot_prime_lift_iff:
1.345 +  assumes p: "prime p" "odd p" and "residue_primroot p g"
1.346 +  shows   "(\<forall>k>0. residue_primroot (p ^ k) g) \<longleftrightarrow> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
1.347 +proof -
1.348 +  from assms have g: "coprime p g" "ord p g = p - 1"
1.349 +    by (auto simp: residue_primroot_def totient_prime)
1.350 +  show ?thesis
1.351 +  proof
1.352 +    assume "\<forall>k>0. residue_primroot (p ^ k) g"
1.353 +    hence "residue_primroot (p\<^sup>2) g" by auto
1.354 +    hence "ord (p\<^sup>2) g = totient (p\<^sup>2)"
1.355 +      by (simp_all add: residue_primroot_def)
1.356 +    thus "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
1.357 +      using g assms prime_gt_1_nat[of p]
1.358 +      by (auto simp: ord_divides' totient_prime_power)
1.359 +  next
1.360 +    assume g': "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
1.361 +
1.362 +    have "residue_primroot (p ^ k) g" if "k > 0" for k
1.363 +    proof (cases "k = 1")
1.364 +      case False
1.365 +      with that have k: "k > 1" by simp
1.366 +      from g have coprime: "coprime (p ^ k) g"
1.367 +        by (auto simp: totatives_def coprime_commute)
1.368 +
1.369 +      define t where "t = ord (p ^ k) g"
1.370 +      have "[g ^ t = 1] (mod (p ^ k))"
1.371 +        by (simp add: t_def ord_divides')
1.372 +      also have "p ^ k = p * p ^ (k - 1)"
1.373 +        using k by (cases k) auto
1.374 +      finally have "[g ^ t = 1] (mod p)"
1.375 +        by (rule cong_modulus_mult_nat)
1.376 +      hence "totient p dvd t"
1.377 +        using g p by (simp add: ord_divides' totient_prime)
1.378 +      then obtain q where t: "t = totient p * q" by auto
1.379 +
1.380 +      have "t dvd totient (p ^ k)"
1.381 +        using coprime by (simp add: t_def order_divides_totient)
1.382 +      with t p k have "q dvd p ^ (k - 1)" using prime_gt_1_nat[of p]
1.383 +        by (auto simp: totient_prime totient_prime_power)
1.384 +      then obtain b where b: "b \<le> k - 1" "q = p ^ b"
1.385 +        using divides_primepow_nat[of p q "k - 1"] p by auto
1.386 +
1.387 +      have "b = k - 1"
1.388 +      proof (rule ccontr)
1.389 +        assume "b \<noteq> k - 1"
1.390 +        with b have "b < k - 1" by simp
1.391 +        have "t = p ^ b * (p - 1)"
1.392 +          using b p by (simp add: t totient_prime)
1.393 +        also have "\<dots> dvd p ^ (k - 2) * (p - 1)"
1.394 +          using \<open>b < k - 1\<close> by (intro mult_dvd_mono le_imp_power_dvd) auto
1.395 +        also have "\<dots> = totient (p ^ (k - 1))"
1.396 +          using k p by (simp add: totient_prime_power numeral_2_eq_2)
1.397 +        finally have "[g ^ totient (p ^ (k - 1)) = 1] (mod (p ^ k))"
1.398 +          by (simp add: ord_divides' t_def)
1.399 +        with residue_primroot_power_prime_power_neq_1[of k p g] p k assms g' show False
1.400 +          by auto
1.401 +      qed
1.402 +      hence "t = totient (p ^ k)"
1.403 +        using p k by (simp add: t b totient_prime totient_prime_power)
1.404 +      thus "residue_primroot (p ^ k) g"
1.405 +        using g one_less_power[of p k] prime_gt_1_nat[of p] p k
1.406 +        by (simp add: residue_primroot_def t_def)
1.407 +    qed (use assms in auto)
1.408 +    thus "\<forall>k>0. residue_primroot (p ^ k) g" by blast
1.409 +  qed
1.410 +qed
1.411 +
1.412 +text \<open>
1.413 +  If \<open>p\<close> is an odd prime, there is always a primitive root \<open>g\<close> modulo \<open>p\<close>, and if \<open>g\<close> does not
1.414 +  fulfil the above assumption required for it to be liftable to $p^k$, we can use $g + p$, which
1.415 +  is also a primitive root modulo \<open>p\<close> and \<^emph>\<open>does\<close> fulfil the assumption.
1.416 +
1.417 +  This shows that any modulus that is a power of an odd prime has a primitive root.
1.418 +\<close>
1.419 +theorem residue_primroot_odd_prime_power_exists:
1.420 +  assumes p: "prime p" "odd p"
1.421 +  obtains g where "\<forall>k>0. residue_primroot (p ^ k) g"
1.422 +proof -
1.423 +  obtain g where g: "residue_primroot p g"
1.424 +    using prime_primitive_root_exists[of p] assms prime_gt_1_nat[of p] by auto
1.425 +
1.426 +  have "\<exists>g. residue_primroot p g \<and> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
1.427 +  proof (cases "[g ^ (p - 1) = 1] (mod p\<^sup>2)")
1.428 +    case True
1.429 +    define g' where "g' = p + g"
1.430 +    note g
1.431 +    also have "residue_primroot p g \<longleftrightarrow> residue_primroot p g'"
1.432 +      unfolding g'_def by (rule residue_primroot_cong) (auto simp: cong_def)
1.433 +    finally have g': "residue_primroot p g'" .
1.434 +
1.435 +    have "[g' ^ (p - 1) = (\<Sum>k\<le>p-1. ((p-1) choose k) * g ^ (p - Suc k) * p ^ k)] (mod p\<^sup>2)"
1.436 +      (is "[_ = ?rhs] (mod _)") by (simp add: g'_def binomial mult_ac)
1.437 +    also have "[?rhs = (\<Sum>k\<le>p-1. if k \<le> 1 then ((p-1) choose k) *
1.438 +                                   g ^ (p - Suc k) * p ^ k else 0)] (mod p\<^sup>2)"
1.439 +      (is "[sum ?f _ = sum ?g _] (mod _)")
1.440 +    proof (intro cong_sum)
1.441 +      fix k assume "k \<in> {..p-1}"
1.442 +      show "[?f k = ?g k] (mod p\<^sup>2)"
1.443 +      proof (cases "k \<le> 1")
1.444 +        case False
1.445 +        have "p\<^sup>2 dvd ?f k"
1.446 +          using False by (intro dvd_mult le_imp_power_dvd) auto
1.447 +        thus ?thesis using False by (simp add: cong_0_iff)
1.448 +      qed auto
1.449 +    qed
1.450 +    also have "sum ?g {..p-1} = sum ?f {0, 1}"
1.451 +      using prime_gt_1_nat[of p] p by (intro sum.mono_neutral_cong_right) auto
1.452 +    also have "\<dots> = g ^ (p - 1) + p * (p - 1) * g ^ (p - 2)"
1.453 +      using p by (simp add: numeral_2_eq_2)
1.454 +    also have "[g ^ (p - 1) + p * (p - 1) * g ^ (p - 2) = 1 + p * (p - 1) * g ^ (p - 2)] (mod p\<^sup>2)"
1.455 +      by (intro cong_add True) auto
1.456 +    finally have "[g' ^ (p - 1) = 1 + p * (p - 1) * g ^ (p - 2)] (mod p\<^sup>2)" .
1.457 +
1.458 +    moreover have "[1 + p * (p - 1) * g ^ (p - 2) \<noteq> 1] (mod p\<^sup>2)"
1.459 +    proof
1.460 +      assume "[1 + p * (p - 1) * g ^ (p - 2) = 1] (mod p\<^sup>2)"
1.461 +      hence "[1 + p * (p - 1) * g ^ (p - 2) - 1 = 1 - 1] (mod p\<^sup>2)"
1.462 +        by (intro cong_diff_nat) auto
1.463 +      hence "p * p dvd p * ((p - 1) * g ^ (p - 2))"
1.464 +        by (auto simp: cong_0_iff power2_eq_square)
1.465 +      hence "p dvd (p - 1) * g ^ (p - 2)"
1.466 +        using p by simp
1.467 +      hence "p dvd g ^ (p - 2)"
1.468 +        using p dvd_imp_le[of p "p - Suc 0"] prime_gt_1_nat[of p]
1.469 +        by (auto simp: prime_dvd_mult_iff)
1.470 +      also have "\<dots> dvd g ^ (p - 1)"
1.471 +        by (intro le_imp_power_dvd) auto
1.472 +      finally have "[g ^ (p - 1) = 0] (mod p)"
1.473 +        by (simp add: cong_0_iff)
1.474 +      hence "[0 = g ^ (p - 1)] (mod p)"
1.475 +        by (simp add: cong_sym_eq)
1.476 +
1.477 +      also from \<open>residue_primroot p g\<close> have "[g ^ (p - 1) = 1] (mod p)"
1.478 +        using p by (auto simp: residue_primroot_def ord_divides' totient_prime)
1.479 +      finally have "[0 = 1] (mod p)" .
1.480 +      thus False using prime_gt_1_nat[of p] p by (simp add: cong_def)
1.481 +    qed
1.482 +
1.483 +    ultimately have "[g' ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
1.484 +      by (simp add: cong_def)
1.485 +    thus "\<exists>g. residue_primroot p g \<and> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
1.486 +      using g' by blast
1.487 +  qed (use g in auto)
1.488 +  thus ?thesis
1.489 +    using residue_primroot_prime_lift_iff[OF assms] that by blast
1.490 +qed
1.491 +
1.492 +
1.493 +subsection \<open>Carmichael's function\<close>
1.494 +
1.495 +text \<open>
1.496 +  Carmichael's function $\lambda(n)$ gives the LCM of the orders of all elements in the
1.497 +  residue ring modulo $n$ -- or, equivalently, the maximum order, as we will show later.
1.498 +  Algebraically speaking, it is the exponent of the multiplicative group
1.499 +  $(\mathbb{Z}/n\mathbb{Z})^*$.
1.500 +
1.501 +  It is not to be confused with Liouville's function, which is also denoted by $\lambda(n)$.
1.502 +\<close>
1.503 +definition Carmichael where
1.504 +  "Carmichael n = (LCM a \<in> totatives n. ord n a)"
1.505 +
1.506 +lemma Carmichael_0 [simp]: "Carmichael 0 = 1"
1.507 +  by (simp add: Carmichael_def)
1.508 +
1.509 +lemma Carmichael_1 [simp]: "Carmichael 1 = 1"
1.510 +  by (simp add: Carmichael_def)
1.511 +
1.512 +lemma Carmichael_Suc_0 [simp]: "Carmichael (Suc 0) = 1"
1.513 +  by (simp add: Carmichael_def)
1.514 +
1.515 +lemma ord_dvd_Carmichael:
1.516 +  assumes "n > 1" "coprime n k"
1.517 +  shows   "ord n k dvd Carmichael n"
1.518 +proof -
1.519 +  have "k mod n \<in> totatives n"
1.520 +    using assms by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I)
1.521 +  hence "ord n (k mod n) dvd Carmichael n"
1.522 +    by (simp add: Carmichael_def del: ord_mod)
1.523 +  thus ?thesis by simp
1.524 +qed
1.525 +
1.526 +lemma Carmichael_divides:
1.527 +  assumes "Carmichael n dvd k" "coprime n a"
1.528 +  shows   "[a ^ k = 1] (mod n)"
1.529 +proof (cases "n < 2 \<or> a = 1")
1.530 +  case False
1.531 +  hence "ord n a dvd Carmichael n"
1.532 +    using False assms by (intro ord_dvd_Carmichael) auto
1.533 +  also have "\<dots> dvd k" by fact
1.534 +  finally have "ord n a dvd k" .
1.535 +  thus ?thesis using ord_divides by auto
1.536 +next
1.537 +  case True
1.538 +  then consider "a = 1" | "n = 0" | "n = 1" by force
1.539 +  thus ?thesis using assms by cases auto
1.540 +qed
1.541 +
1.542 +lemma Carmichael_dvd_totient: "Carmichael n dvd totient n"
1.543 +  unfolding Carmichael_def
1.544 +proof (intro Lcm_least, safe)
1.545 +  fix a assume "a \<in> totatives n"
1.546 +  hence "[a ^ totient n = 1] (mod n)"
1.547 +    by (intro euler_theorem) (auto simp: totatives_def)
1.548 +  thus "ord n a dvd totient n"
1.549 +    using ord_divides by blast
1.550 +qed
1.551 +
1.552 +lemma Carmichael_dvd_mono_coprime:
1.553 +  assumes "coprime m n" "m > 1" "n > 1"
1.554 +  shows   "Carmichael m dvd Carmichael (m * n)"
1.555 +  unfolding Carmichael_def[of m]
1.556 +proof (intro Lcm_least, safe)
1.557 +  fix x assume x: "x \<in> totatives m"
1.558 +  from assms have "totatives n \<noteq> {}" by simp
1.559 +  then obtain y where y: "y \<in> totatives n" by blast
1.560 +
1.561 +  from binary_chinese_remainder_nat[OF assms(1), of x y]
1.562 +  obtain z where z: "[z = x] (mod m)" "[z = y] (mod n)" by blast
1.563 +  have z': "coprime z n" "coprime z m"
1.564 +    by (rule cong_imp_coprime; use x y z in \<open>force simp: totatives_def cong_sym_eq\<close>)+
1.565 +
1.566 +  from z have "ord m x = ord m z"
1.567 +    by (intro ord_cong) (auto simp: cong_sym_eq)
1.568 +  also have "ord m z dvd ord (m * n) z"
1.569 +    using assms by (auto simp: ord_modulus_mult_coprime)
1.570 +  also from z' assms have "\<dots> dvd Carmichael (m * n)"
1.571 +    by (intro ord_dvd_Carmichael) (auto simp: coprime_commute intro!:one_less_mult)
1.572 +  finally show "ord m x dvd Carmichael (m * n)" .
1.573 +qed
1.574 +
1.575 +text \<open>
1.576 +  $\lambda$ distributes over the product of coprime numbers similarly to $\varphi$, but
1.577 +  with LCM instead of multiplication:
1.578 +\<close>
1.579 +lemma Carmichael_mult_coprime:
1.580 +  assumes "coprime m n"
1.581 +  shows   "Carmichael (m * n) = lcm (Carmichael m) (Carmichael n)"
1.582 +proof (cases "m \<le> 1 \<or> n \<le> 1")
1.583 +  case True
1.584 +  hence "m = 0 \<or> n = 0 \<or> m = 1 \<or> n = 1" by force
1.585 +  thus ?thesis using assms by auto
1.586 +next
1.587 +  case False
1.588 +  show ?thesis
1.589 +  proof (rule dvd_antisym)
1.590 +    show "Carmichael (m * n) dvd lcm (Carmichael m) (Carmichael n)"
1.591 +      unfolding Carmichael_def[of "m * n"]
1.592 +    proof (intro Lcm_least, safe)
1.593 +      fix x assume x: "x \<in> totatives (m * n)"
1.594 +      have "ord (m * n) x = lcm (ord m x) (ord n x)"
1.595 +        using assms x by (subst ord_modulus_mult_coprime) (auto simp: coprime_commute totatives_def)
1.596 +      also have "\<dots> dvd lcm (Carmichael m) (Carmichael n)"
1.597 +        using False x
1.598 +        by (intro lcm_mono ord_dvd_Carmichael) (auto simp: totatives_def coprime_commute)
1.599 +      finally show "ord (m * n) x dvd \<dots>" .
1.600 +    qed
1.601 +  next
1.602 +    show "lcm (Carmichael m) (Carmichael n) dvd Carmichael (m * n)"
1.603 +      using Carmichael_dvd_mono_coprime[of m n]
1.604 +            Carmichael_dvd_mono_coprime[of n m] assms False
1.605 +      by (auto intro!: lcm_least simp: coprime_commute mult.commute)
1.606 +  qed
1.607 +qed
1.608 +
1.609 +lemma Carmichael_pos [simp, intro]: "Carmichael n > 0"
1.610 +  by (auto simp: Carmichael_def ord_eq_0 totatives_def coprime_commute intro!: Nat.gr0I)
1.611 +
1.612 +lemma Carmichael_nonzero [simp]: "Carmichael n \<noteq> 0"
1.613 +  by simp
1.614 +
1.615 +lemma power_Carmichael_eq_1:
1.616 +  assumes "n > 1" "coprime n x"
1.617 +  shows   "[x ^ Carmichael n = 1] (mod n)"
1.618 +  using ord_dvd_Carmichael[of n x] assms
1.619 +  by (auto simp: ord_divides')
1.620 +
1.621 +lemma Carmichael_2 [simp]: "Carmichael 2 = 1"
1.622 +  using Carmichael_dvd_totient[of 2] by simp
1.623 +
1.624 +lemma Carmichael_4 [simp]: "Carmichael 4 = 2"
1.625 +proof -
1.626 +  have "Carmichael 4 dvd 2"
1.627 +    using Carmichael_dvd_totient[of 4] by simp
1.628 +  hence "Carmichael 4 \<le> 2" by (rule dvd_imp_le) auto
1.629 +  moreover have "Carmichael 4 \<noteq> 1"
1.630 +    using power_Carmichael_eq_1[of "4::nat" 3]
1.631 +    unfolding coprime_iff_gcd_eq_1 by (auto simp: gcd_non_0_nat cong_def)
1.632 +  ultimately show ?thesis
1.633 +    using Carmichael_pos[of 4] by linarith
1.634 +qed
1.635 +
1.636 +lemma residue_primroot_Carmichael:
1.637 +  assumes "residue_primroot n g"
1.638 +  shows   "Carmichael n = totient n"
1.639 +proof (cases "n = 1")
1.640 +  case False
1.641 +  show ?thesis
1.642 +  proof (intro dvd_antisym Carmichael_dvd_totient)
1.643 +    have "ord n g dvd Carmichael n"
1.644 +      using assms False by (intro ord_dvd_Carmichael) (auto simp: residue_primroot_def)
1.645 +    thus "totient n dvd Carmichael n"
1.646 +      using assms by (auto simp: residue_primroot_def)
1.647 +  qed
1.648 +qed auto
1.649 +
1.650 +lemma Carmichael_odd_prime_power:
1.651 +  assumes "prime p" "odd p" "k > 0"
1.652 +  shows   "Carmichael (p ^ k) = p ^ (k - 1) * (p - 1)"
1.653 +proof -
1.654 +  from assms obtain g where "residue_primroot (p ^ k) g"
1.655 +    using residue_primroot_odd_prime_power_exists[of p] assms by metis
1.656 +  hence "Carmichael (p ^ k) = totient (p ^ k)"
1.657 +    by (intro residue_primroot_Carmichael[of "p ^ k" g]) auto
1.658 +  with assms show ?thesis by (simp add: totient_prime_power)
1.659 +qed
1.660 +
1.661 +lemma Carmichael_prime:
1.662 +  assumes "prime p"
1.663 +  shows   "Carmichael p = p - 1"
1.664 +proof (cases "even p")
1.665 +  case True
1.666 +  with assms have "p = 2"
1.667 +    using primes_dvd_imp_eq two_is_prime_nat by blast
1.668 +  thus ?thesis by simp
1.669 +next
1.670 +  case False
1.671 +  with Carmichael_odd_prime_power[of p 1] assms show ?thesis by simp
1.672 +qed
1.673 +
1.674 +lemma Carmichael_twopow_ge_8:
1.675 +  assumes "k \<ge> 3"
1.676 +  shows   "Carmichael (2 ^ k) = 2 ^ (k - 2)"
1.677 +proof (intro dvd_antisym)
1.678 +  have "2 ^ (k - 2) = ord (2 ^ k) (3 :: nat)"
1.679 +    using ord_twopow_3_5[of k 3] assms by simp
1.680 +  also have "\<dots> dvd Carmichael (2 ^ k)"
1.681 +    using assms one_less_power[of "2::nat" k] by (intro ord_dvd_Carmichael) auto
1.682 +  finally show "2 ^ (k - 2) dvd \<dots>" .
1.683 +next
1.684 +  show "Carmichael (2 ^ k) dvd 2 ^ (k - 2)"
1.685 +    unfolding Carmichael_def
1.686 +  proof (intro Lcm_least, safe)
1.687 +    fix x assume "x \<in> totatives (2 ^ k)"
1.688 +    hence "odd x" by (auto simp: totatives_def)
1.689 +    hence "[x ^ 2 ^ (k - 2) = 1] (mod 2 ^ k)"
1.690 +      using assms ord_twopow_aux[of k x] by auto
1.691 +    thus "ord (2 ^ k) x dvd 2 ^ (k - 2)"
1.692 +      by (simp add: ord_divides')
1.693 +  qed
1.694 +qed
1.695 +
1.696 +lemma Carmichael_twopow:
1.697 +  "Carmichael (2 ^ k) = (if k \<le> 2 then 2 ^ (k - 1) else 2 ^ (k - 2))"
1.698 +proof -
1.699 +  have "k = 0 \<or> k = 1 \<or> k = 2 \<or> k \<ge> 3" by linarith
1.700 +  thus ?thesis by (auto simp: Carmichael_twopow_ge_8)
1.701 +qed
1.702 +
1.703 +lemma Carmichael_prime_power:
1.704 +  assumes "prime p" "k > 0"
1.705 +  shows   "Carmichael (p ^ k) =
1.706 +             (if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
1.707 +proof (cases "p = 2")
1.708 +  case True
1.709 +  thus ?thesis by (simp add: Carmichael_twopow)
1.710 +next
1.711 +  case False
1.712 +  with assms have "odd p" "p > 2"
1.713 +    using prime_odd_nat[of p] prime_gt_1_nat[of p] by auto
1.714 +  thus ?thesis
1.715 +    using assms Carmichael_odd_prime_power[of p k] by simp
1.716 +qed
1.717 +
1.718 +lemma Carmichael_prod_coprime:
1.719 +  assumes "finite A" "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i \<noteq> j \<Longrightarrow> coprime (f i) (f j)"
1.720 +  shows   "Carmichael (\<Prod>i\<in>A. f i) = (LCM i\<in>A. Carmichael (f i))"
1.721 +  using assms by (induction A rule: finite_induct)
1.722 +                 (simp, simp, subst Carmichael_mult_coprime[OF prod_coprime_right], auto)
1.723 +
1.724 +text \<open>
1.725 +  Since $\lambda$ distributes over coprime factors and we know the value of $\lambda(p^k)$
1.726 +  for prime $p$, we can now give a closed formula for $\lambda(n)$ in terms of the prime
1.727 +  factorisation of $n$:
1.728 +\<close>
1.729 +theorem Carmichael_closed_formula:
1.730 +  "Carmichael n =
1.731 +     (LCM p\<in>prime_factors n. let k = multiplicity p n
1.732 +                             in  if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
1.733 +  (is "_ = Lcm ?A")
1.734 +proof (cases "n = 0")
1.735 +  case False
1.736 +  hence "n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
1.737 +    using prime_factorization_nat by blast
1.738 +  also have "Carmichael \<dots> =
1.739 +               (LCM p\<in>prime_factors n. Carmichael (p ^ multiplicity p n))"
1.740 +    by (subst Carmichael_prod_coprime) (auto simp: in_prime_factors_iff primes_coprime)
1.741 +  also have "(\<lambda>p. Carmichael (p ^ multiplicity p n))  prime_factors n = ?A"
1.742 +    by (intro image_cong)
1.743 +       (auto simp: Let_def Carmichael_prime_power prime_factors_multiplicity)
1.744 +  finally show ?thesis .
1.745 +qed auto
1.746 +
1.747 +corollary even_Carmichael:
1.748 +  assumes "n > 2"
1.749 +  shows   "even (Carmichael n)"
1.750 +proof (cases "\<exists>k. n = 2 ^ k")
1.751 +  case True
1.752 +  then obtain k where [simp]: "n = 2 ^ k" by auto
1.753 +  from assms have "k \<noteq> 0" "k \<noteq> 1" by (auto intro!: Nat.gr0I)
1.754 +  hence "k \<ge> 2" by auto
1.755 +  thus ?thesis by (auto simp: Carmichael_twopow)
1.756 +next
1.757 +  case False
1.758 +  from assms have "n \<noteq> 0" by auto
1.759 +  from False have "\<exists>p\<in>prime_factors n. p \<noteq> 2"
1.760 +    using assms Ex_other_prime_factor[of n 2] by auto
1.761 +  from divide_out_primepow_ex[OF \<open>n \<noteq> 0\<close> this] guess p k n' . note p = this
1.762 +  from p have coprime: "coprime (p ^ k) n'"
1.763 +    using p prime_imp_coprime by auto
1.764 +  have "odd p"
1.765 +    using p primes_dvd_imp_eq[of 2 p] by auto
1.766 +  have "even (Carmichael (p ^ k))"
1.767 +    using p \<open>odd p\<close> by (auto simp: Carmichael_prime_power)
1.768 +  with p coprime show ?thesis
1.769 +    by (auto simp: Carmichael_mult_coprime intro!: dvd_lcmI1)
1.770 +qed
1.771 +
1.772 +lemma eval_Carmichael:
1.773 +  assumes "prime_factorization n = A"
1.774 +  shows     "Carmichael n = (LCM p \<in> set_mset A.
1.775 +               let k = count A p in if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
1.776 +  unfolding assms [symmetric] Carmichael_closed_formula
1.777 +  by (intro arg_cong[where f = Lcm] image_cong) (auto simp: Let_def count_prime_factorization)
1.778 +
1.779 +text \<open>
1.780 +  Any residue ring always contains a $\lambda$-root, i.\,e.\ an element whose
1.781 +  order is $\lambda(n)$.
1.782 +\<close>
1.783 +theorem Carmichael_root_exists:
1.784 +  assumes "n > (0::nat)"
1.785 +  obtains g where "g \<in> totatives n" and "ord n g = Carmichael n"
1.786 +proof (cases "n = 1")
1.787 +  case True
1.788 +  thus ?thesis by (intro that[of 1]) (auto simp: totatives_def)
1.789 +next
1.790 +  case False
1.791 +  have primepow: "\<exists>g. coprime (p ^ k) g \<and> ord (p ^ k) g = Carmichael (p ^ k)"
1.792 +    if pk: "prime p" "k > 0" for p k
1.793 +  proof (cases "p = 2")
1.794 +    case [simp]: True
1.795 +    from \<open>k > 0\<close> consider "k = 1" | "k = 2" | "k \<ge> 3" by force
1.796 +    thus ?thesis
1.797 +    proof cases
1.798 +      assume "k = 1"
1.799 +      thus ?thesis by (intro exI[of _ 1]) auto
1.800 +    next
1.801 +      assume [simp]: "k = 2"
1.802 +      have "coprime 4 (3::nat)"
1.803 +        by (auto simp: coprime_iff_gcd_eq_1 gcd_non_0_nat)
1.804 +      thus ?thesis by (intro exI[of _ 3]) auto
1.805 +    next
1.806 +      assume k: "k \<ge> 3"
1.807 +      have "coprime (2 ^ k :: nat) 3" by auto
1.808 +      thus ?thesis using k
1.809 +        by (intro exI[of _ 3]) (auto simp: ord_twopow_3_5 Carmichael_twopow)
1.810 +    qed
1.811 +  next
1.812 +    case False
1.813 +    hence "odd p" using \<open>prime p\<close>
1.814 +      using primes_dvd_imp_eq two_is_prime_nat by blast
1.815 +    then obtain g where "residue_primroot (p ^ k) g"
1.816 +      using residue_primroot_odd_prime_power_exists[of p] pk by metis
1.817 +    thus ?thesis using False pk
1.818 +      by (intro exI[of _ g])
1.819 +         (auto simp: Carmichael_prime_power residue_primroot_def totient_prime_power)
1.820 +  qed
1.821 +
1.822 +  define P where "P = prime_factors n"
1.823 +  define k where "k = (\<lambda>p. multiplicity p n)"
1.824 +  have "\<forall>p\<in>P. \<exists>g. coprime (p ^ k p) g \<and> ord (p ^ k p) g = Carmichael (p ^ k p)"
1.825 +    using primepow by (auto simp: P_def k_def prime_factors_multiplicity)
1.826 +  hence "\<exists>g. \<forall>p\<in>P. coprime (p ^ k p) (g p) \<and> ord (p ^ k p) (g p) = Carmichael (p ^ k p)"
1.827 +    by (subst (asm) bchoice_iff)
1.828 +  then obtain g where g: "\<And>p. p \<in> P \<Longrightarrow> coprime (p ^ k p) (g p)"
1.829 +                         "\<And>p. p \<in> P \<Longrightarrow> ord (p ^ k p) (g p) = Carmichael (p ^ k p)" by metis
1.830 +  have "\<exists>x. \<forall>i\<in>P. [x = g i] (mod i ^ k i)"
1.831 +    by (intro chinese_remainder_nat)
1.832 +       (auto simp: P_def k_def in_prime_factors_iff primes_coprime)
1.833 +  then obtain x where x: "\<And>p. p \<in> P \<Longrightarrow> [x = g p] (mod p ^ k p)" by metis
1.834 +
1.835 +  have "n = (\<Prod>p\<in>P. p ^ k p)"
1.836 +    using assms unfolding P_def k_def by (rule prime_factorization_nat)
1.837 +  also have "ord \<dots> x = (LCM p\<in>P. ord (p ^ k p) x)"
1.838 +    by (intro ord_modulus_prod_coprime) (auto simp: P_def in_prime_factors_iff primes_coprime)
1.839 +  also have "(\<lambda>p. ord (p ^ k p) x)  P = (\<lambda>p. ord (p ^ k p) (g p))  P"
1.840 +    by (intro image_cong ord_cong x) auto
1.841 +  also have "\<dots> = (\<lambda>p. Carmichael (p ^ k p))  P"
1.842 +    by (intro image_cong g) auto
1.843 +  also have "Lcm \<dots> = Carmichael (\<Prod>p\<in>P. p ^ k p)"
1.844 +    by (intro Carmichael_prod_coprime [symmetric])
1.845 +       (auto simp: P_def in_prime_factors_iff primes_coprime)
1.846 +  also have "(\<Prod>p\<in>P. p ^ k p) = n"
1.847 +    using assms unfolding P_def k_def by (rule prime_factorization_nat [symmetric])
1.848 +  finally have "ord n x = Carmichael n" .
1.849 +  moreover from this have "coprime n x"
1.850 +    by (cases "coprime n x") (auto split: if_splits)
1.851 +  ultimately show ?thesis using assms False
1.852 +    by (intro that[of "x mod n"])
1.853 +       (auto simp: totatives_def coprime_commute coprime_absorb_left intro!: Nat.gr0I)
1.854 +qed
1.855 +
1.856 +text \<open>
1.857 +  This also means that the Carmichael number is not only the LCM of the orders
1.858 +  of the elements of the residue ring, but indeed the maximum of the orders.
1.859 +\<close>
1.860 +lemma Carmichael_altdef:
1.861 +  "Carmichael n = (if n = 0 then 1 else Max (ord n  totatives n))"
1.862 +proof (cases "n = 0")
1.863 +  case False
1.864 +  have "Carmichael n = Max (ord n  totatives n)"
1.865 +  proof (intro antisym Max.boundedI Max.coboundedI)
1.866 +    fix k assume k: "k \<in> ord n  totatives n"
1.867 +    thus "k \<le> Carmichael n"
1.868 +    proof (cases "n = 1")
1.869 +      case False
1.870 +      with \<open>n \<noteq> 0\<close> have "n > 1" by linarith
1.871 +      thus ?thesis using k \<open>n \<noteq> 0\<close>
1.872 +        by (intro dvd_imp_le)
1.873 +           (auto intro!: ord_dvd_Carmichael simp: totatives_def coprime_commute)
1.874 +    qed auto
1.875 +  next
1.876 +    obtain g where "g \<in> totatives n" and "ord n g = Carmichael n"
1.877 +      using Carmichael_root_exists[of n] \<open>n \<noteq> 0\<close> by auto
1.878 +    thus "Carmichael n \<in> ord n  totatives n" by force
1.879 +  qed (use \<open>n \<noteq> 0\<close> in auto)
1.880 +  thus ?thesis using False by simp
1.881 +qed auto
1.882 +
1.883 +
1.884 +subsection \<open>Existence of primitive roots for general moduli\<close>
1.885 +
1.886 +text \<open>
1.887 +  We now related Carmichael's function to the existence of primitive roots and, in the end,
1.888 +  use this to show precisely which moduli have primitive roots and which do not.
1.889 +
1.890 +  The first criterion for the existence of a primitive root is this: A primitive root modulo $n$
1.891 +  exists iff $\lambda(n) = \varphi(n)$.
1.892 +\<close>
1.893 +lemma Carmichael_eq_totient_imp_primroot:
1.894 +  assumes "n > 0" and "Carmichael n = totient n"
1.895 +  shows   "\<exists>g. residue_primroot n g"
1.896 +proof -
1.897 +  from \<open>n > 0\<close> obtain g where "g \<in> totatives n" and "ord n g = Carmichael n"
1.898 +    using Carmichael_root_exists[of n] by metis
1.899 +  with assms show ?thesis by (auto simp: residue_primroot_def totatives_def coprime_commute)
1.900 +qed
1.901 +
1.902 +theorem residue_primroot_iff_Carmichael:
1.903 +  "(\<exists>g. residue_primroot n g) \<longleftrightarrow> Carmichael n = totient n \<and> n > 0"
1.904 +proof safe
1.905 +  fix g assume g: "residue_primroot n g"
1.906 +  thus "n > 0" by (auto simp: residue_primroot_def)
1.907 +  have "coprime n g" by (rule ccontr) (use g in \<open>auto simp: residue_primroot_def\<close>)
1.908 +
1.909 +  show "Carmichael n = totient n"
1.910 +  proof (cases "n = 1")
1.911 +    case False
1.912 +    with \<open>n > 0\<close> have "n > 1" by auto
1.913 +    with \<open>coprime n g\<close> have "ord n g dvd Carmichael n"
1.914 +      by (intro ord_dvd_Carmichael) auto
1.915 +    thus ?thesis using g by (intro dvd_antisym Carmichael_dvd_totient)
1.916 +                            (auto simp: residue_primroot_def)
1.917 +  qed auto
1.918 +qed (use Carmichael_eq_totient_imp_primroot[of n] in auto)
1.919 +
1.920 +text \<open>
1.921 +  Any primitive root modulo $mn$ for coprime $m$, $n$ is also a primitive root modulo $m$ and $n$.
1.922 +  The converse does not hold in general.
1.923 +\<close>
1.924 +lemma residue_primroot_modulus_mult_coprimeD:
1.925 +  assumes "coprime m n" and "residue_primroot (m * n) g"
1.926 +  shows   "residue_primroot m g" "residue_primroot n g"
1.927 +proof -
1.928 +  have *: "m > 0" "n > 0" "coprime m g" "coprime n g"
1.929 +          "lcm (ord m g) (ord n g) = totient m * totient n"
1.930 +    using assms
1.931 +    by (auto simp: residue_primroot_def ord_modulus_mult_coprime totient_mult_coprime)
1.932 +
1.933 +  define a b where "a = totient m div ord m g" and "b = totient n div ord n g"
1.934 +  have ab: "totient m = ord m g * a" "totient n = ord n g * b"
1.935 +    using * by (auto simp: a_def b_def order_divides_totient)
1.936 +
1.937 +  have "a = 1" "b = 1" "coprime (ord m g) (ord n g)"
1.938 +    unfolding coprime_iff_gcd_eq_1 using * by (auto simp: ab lcm_nat_def dvd_div_eq_mult ord_eq_0)
1.939 +  with ab and * show "residue_primroot m g" "residue_primroot n g"
1.940 +    by (auto simp: residue_primroot_def)
1.941 +qed
1.942 +
1.943 +text \<open>
1.944 +  If a primitive root modulo $mn$ exists for coprime $m, n$, then $\lambda(m)$ and $\lambda(n)$
1.945 +  must also be coprime. This is helpful in establishing that there are no primitive roots
1.946 +  modulo $mn$ by showing e.\,g.\ that $\lambda(m)$ and $\lambda(n)$ are both even.
1.947 +\<close>
1.948 +lemma residue_primroot_modulus_mult_coprime_imp_Carmichael_coprime:
1.949 +  assumes "coprime m n" and "residue_primroot (m * n) g"
1.950 +  shows   "coprime (Carmichael m) (Carmichael n)"
1.951 +proof -
1.952 +  from residue_primroot_modulus_mult_coprimeD[OF assms]
1.953 +    have *: "residue_primroot m g" "residue_primroot n g" by auto
1.954 +  hence [simp]: "Carmichael m = totient m" "Carmichael n = totient n"
1.955 +    by (simp_all add: residue_primroot_Carmichael)
1.956 +  from * have mn: "m > 0" "n > 0" by (auto simp: residue_primroot_def)
1.957 +
1.958 +  from assms have "Carmichael (m * n) = totient (m * n) \<and> n > 0"
1.959 +    using residue_primroot_iff_Carmichael[of "m * n"] by auto
1.960 +  with assms have "lcm (totient m) (totient n) = totient m * totient n"
1.961 +    by (simp add: Carmichael_mult_coprime totient_mult_coprime)
1.962 +  thus ?thesis unfolding coprime_iff_gcd_eq_1 using mn
1.963 +    by (simp add: lcm_nat_def dvd_div_eq_mult)
1.964 +qed
1.965 +
1.966 +text \<open>
1.967 +  The following moduli are precisely those that have primitive roots.
1.968 +\<close>
1.969 +definition cyclic_moduli :: "nat set" where
1.970 +  "cyclic_moduli = {1, 2, 4} \<union> {p ^ k |p k. prime p \<and> odd p \<and> k > 0} \<union>
1.971 +                     {2 * p ^ k |p k. prime p \<and> odd p \<and> k > 0}"
1.972 +
1.973 +theorem residue_primroot_iff_in_cyclic_moduli:
1.974 +  "(\<exists>g. residue_primroot m g) \<longleftrightarrow> m \<in> cyclic_moduli"
1.975 +proof -
1.976 +  have "(\<exists>g. residue_primroot m g)" if "m \<in> cyclic_moduli"
1.977 +  using that unfolding cyclic_moduli_def
1.978 +  by (intro Carmichael_eq_totient_imp_primroot)
1.979 +     (auto dest: prime_gt_0_nat simp: Carmichael_prime_power totient_prime_power
1.980 +                 Carmichael_mult_coprime totient_mult_coprime)
1.981 +
1.982 +  moreover have "\<not>(\<exists>g. residue_primroot m g)" if "m \<notin> cyclic_moduli"
1.983 +  proof (cases "m = 0")
1.984 +    case False
1.985 +    with that have [simp]: "m > 0" "m \<noteq> 1" by (auto simp: cyclic_moduli_def)
1.986 +    show ?thesis
1.987 +    proof (cases "\<exists>k. m = 2 ^ k")
1.988 +      case True
1.989 +      then obtain k where [simp]: "m = 2 ^ k" by auto
1.990 +      with that have "k \<noteq> 0 \<and> k \<noteq> 1 \<and> k \<noteq> 2" by (auto simp: cyclic_moduli_def)
1.991 +      hence "k \<ge> 3" by auto
1.992 +      thus ?thesis by (subst residue_primroot_iff_Carmichael)
1.993 +                      (auto simp: Carmichael_twopow totient_prime_power)
1.994 +    next
1.995 +      case False
1.996 +      hence "\<exists>p\<in>prime_factors m. p \<noteq> 2"
1.997 +        using Ex_other_prime_factor[of m 2] by auto
1.998 +      from divide_out_primepow_ex[OF \<open>m \<noteq> 0\<close> this]
1.999 +      obtain p k m' where p: "p \<noteq> 2" "prime p" "p dvd m" "\<not>p dvd m'" "0 < k" "m = p ^ k * m'"
1.1000 +        by metis
1.1001 +      have "odd p"
1.1002 +        using p primes_dvd_imp_eq[of 2 p] by auto
1.1003 +      from p have coprime: "coprime (p ^ k) m'"
1.1004 +        using p prime_imp_coprime by auto
1.1005 +      have "m \<in> cyclic_moduli" if "m' = 1"
1.1006 +        using that p \<open>odd p\<close> by (auto simp: cyclic_moduli_def)
1.1007 +      moreover have "m \<in> cyclic_moduli" if "m' = 2"
1.1008 +      proof -
1.1009 +        have "m = 2 * p ^ k" using p that by (simp add: mult.commute)
1.1010 +        thus "m \<in> cyclic_moduli" using p \<open>odd p\<close>
1.1011 +          unfolding cyclic_moduli_def by blast
1.1012 +      qed
1.1013 +      moreover have "m' \<noteq> 0" using p by (intro notI) auto
1.1014 +      ultimately have "m' \<noteq> 0 \<and>m' \<noteq> 1 \<and> m' \<noteq> 2" using that by auto
1.1015 +      hence "m' > 2" by linarith
1.1016 +
1.1017 +      show ?thesis
1.1018 +      proof
1.1019 +        assume "\<exists>g. residue_primroot m g"
1.1020 +        with coprime p have coprime': "coprime (p - 1) (Carmichael m')"
1.1021 +          using residue_primroot_modulus_mult_coprime_imp_Carmichael_coprime[OF coprime]
1.1022 +          by (auto simp: Carmichael_prime_power)
1.1023 +        moreover have "even (p - 1)" "even (Carmichael m')"
1.1024 +          using \<open>m' > 2\<close> \<open>odd p\<close> by (auto intro!: even_Carmichael)
1.1025 +        ultimately show False by force
1.1026 +      qed
1.1027 +    qed
1.1028 +  qed auto
1.1029 +
1.1030 +  ultimately show ?thesis by metis
1.1031 +qed
1.1032 +
1.1033 +lemma residue_primroot_is_generator:
1.1034 +  assumes "m > 1" and "residue_primroot m g"
1.1035 +  shows   "bij_betw (\<lambda>i. g ^ i mod m) {..<totient m} (totatives m)"
1.1036 +  unfolding bij_betw_def
1.1037 +proof
1.1038 +  from assms have [simp]: "ord m g = totient m"
1.1039 +    by (simp add: residue_primroot_def)
1.1040 +  from assms have "coprime m g" by (simp add: residue_primroot_def)
1.1041 +  hence "inj_on (\<lambda>i. g ^ i mod m) {..<ord m g}"
1.1042 +    by (intro inj_power_mod)
1.1043 +  thus inj: "inj_on (\<lambda>i. g ^ i mod m) {..<totient m}"
1.1044 +    by simp
1.1045 +
1.1046 +  show "(\<lambda>i. g ^ i mod m)  {..<totient m} = totatives m"
1.1047 +  proof (rule card_subset_eq)
1.1048 +    show "card ((\<lambda>i. g ^ i mod m)  {..<totient m}) = card (totatives m)"
1.1049 +      using inj by (subst card_image) (auto simp: totient_def)
1.1050 +    show "(\<lambda>i. g ^ i mod m)  {..<totient m} \<subseteq> totatives m"
1.1051 +      using \<open>m > 1\<close> \<open>coprime m g\<close> power_in_totatives[of m g] by blast
1.1052 +  qed auto
1.1053 +qed
1.1054 +
1.1055 +text \<open>
1.1056 +  Given one primitive root \<open>g\<close>, all the primitive roots are powers $g^i$ for
1.1057 +  $1\leq i \leq \varphi(n)$ with $\text{gcd}(i, \varphi(n)) = 1$.
1.1058 +\<close>
1.1059 +theorem residue_primroot_bij_betw_primroots:
1.1060 +  assumes "m > 1" and "residue_primroot m g"
1.1061 +  shows   "bij_betw (\<lambda>i. g ^ i mod m) (totatives (totient m))
1.1062 +                                      {g\<in>totatives m. residue_primroot m g}"
1.1063 +proof (cases "m = 2")
1.1064 +  case [simp]: True
1.1065 +  have [simp]: "totatives 2 = {1}"
1.1066 +    by (auto simp: totatives_def elim!: oddE)
1.1067 +  from assms have "odd g"
1.1068 +    by (auto simp: residue_primroot_def)
1.1069 +  hence pow_eq: "(\<lambda>i. g ^ i mod m) = (\<lambda>_. 1)"
1.1070 +    by (auto simp: fun_eq_iff mod_2_eq_odd)
1.1071 +  have "{g \<in> totatives m. residue_primroot m g} = {1}"
1.1072 +    by (auto simp: residue_primroot_def)
1.1073 +  thus ?thesis using pow_eq by (auto simp: bij_betw_def)
1.1074 +next
1.1075 +  case False
1.1076 +  thus ?thesis unfolding bij_betw_def
1.1077 +  proof safe
1.1078 +    from assms False have "m > 2" by auto
1.1079 +    from assms \<open>m > 2\<close> have "totient m > 1" by (intro totient_gt_1) auto
1.1080 +    from assms have [simp]: "ord m g = totient m"
1.1081 +      by (simp add: residue_primroot_def)
1.1082 +    from assms have "coprime m g" by (simp add: residue_primroot_def)
1.1083 +    hence "inj_on (\<lambda>i. g ^ i mod m) {..<ord m g}"
1.1084 +      by (intro inj_power_mod)
1.1085 +    thus "inj_on (\<lambda>i. g ^ i mod m) (totatives (totient m))"
1.1086 +      by (rule inj_on_subset)
1.1087 +         (use assms \<open>totient m > 1\<close> in \<open>auto simp: totatives_less residue_primroot_def\<close>)
1.1088 +
1.1089 +    {
1.1090 +      fix i assume i: "i \<in> totatives (totient m)"
1.1091 +      from \<open>coprime m g\<close> and \<open>m > 2\<close> show "g ^ i mod m \<in> totatives m"
1.1092 +        by (intro power_in_totatives) auto
1.1093 +      show "residue_primroot m (g ^ i mod m)"
1.1094 +        using i \<open>m > 2\<close> \<open>coprime m g\<close>
1.1095 +        by (auto simp: residue_primroot_def coprime_commute ord_power totatives_def)
1.1096 +    }
1.1097 +    {
1.1098 +      fix x assume x: "x \<in> totatives m" "residue_primroot m x"
1.1099 +      then obtain i where i: "i < totient m" "x = (g ^ i mod m)"
1.1100 +        using assms residue_primroot_is_generator[of m g] by (auto simp: bij_betw_def)
1.1101 +      from i x \<open>m > 2\<close> have "i > 0" by (intro Nat.gr0I) (auto simp: residue_primroot_1_iff)
1.1102 +      have "totient m div gcd i (totient m) = totient m"
1.1103 +        using x i \<open>coprime m g\<close> by (auto simp add: residue_primroot_def ord_power)
1.1104 +      hence "coprime i (totient m)"
1.1105 +        unfolding coprime_iff_gcd_eq_1 using assms by (subst (asm) dvd_div_eq_mult) auto
1.1106 +      with i \<open>i > 0\<close> have "i \<in> totatives (totient m)" by (auto simp: totatives_def)
1.1107 +      thus "x \<in> (\<lambda>i. g ^ i mod m)  totatives (totient m)" using i by auto
1.1108 +    }
1.1109 +  qed
1.1110 +qed
1.1111 +
1.1112 +text \<open>
1.1113 +  It follows from the above statement that any residue ring modulo \<open>n\<close> that \<^emph>\<open>has\<close> primitive roots
1.1114 +  has exactly $\varphi(\varphi(n))$ of them.
1.1115 +\<close>
1.1116 +corollary card_residue_primroots:
1.1117 +  assumes "\<exists>g. residue_primroot m g"
1.1118 +  shows   "card {g\<in>totatives m. residue_primroot m g} = totient (totient m)"
1.1119 +proof (cases "m = 1")
1.1120 +  case [simp]: True
1.1121 +  have "{g \<in> totatives m. residue_primroot m g} = {1}"
1.1122 +    by (auto simp: residue_primroot_def)
1.1123 +  thus ?thesis by simp
1.1124 +next
1.1125 +  case False
1.1126 +  from assms obtain g where g: "residue_primroot m g" by auto
1.1127 +  hence "m \<noteq> 0" by (intro notI) auto
1.1128 +  with \<open>m \<noteq> 1\<close> have "m > 1" by linarith
1.1129 +  from this g have "bij_betw (\<lambda>i. g ^ i mod m) (totatives (totient m))
1.1130 +                      {g\<in>totatives m. residue_primroot m g}"
1.1131 +    by (rule residue_primroot_bij_betw_primroots)
1.1132 +  hence "card (totatives (totient m)) = card {g\<in>totatives m. residue_primroot m g}"
1.1133 +    by (rule bij_betw_same_card)
1.1134 +  thus ?thesis by (simp add: totient_def)
1.1135 +qed
1.1136 +
1.1137 +corollary card_residue_primroots':
1.1138 +  "card {g\<in>totatives m. residue_primroot m g} =
1.1139 +     (if m \<in> cyclic_moduli then totient (totient m) else 0)"
1.1140 +  by (simp add: residue_primroot_iff_in_cyclic_moduli [symmetric] card_residue_primroots)
1.1141 +
1.1142 +text \<open>
1.1143 +  As an example, we evaluate $\lambda(122200)$ using the prime factorisation.
1.1144 +\<close>
1.1145 +lemma "Carmichael 122200 = 1380"
1.1146 +proof -
1.1147 +  have "prime_factorization (2^3 * 5^2 * 13 * 47) = {#2, 2, 2, 5, 5, 13, 47::nat#}"
1.1148 +    by (intro prime_factorization_eqI) auto
1.1149 +  from eval_Carmichael[OF this] show "Carmichael 122200 = 1380"
1.1150 +    by (simp add: lcm_nat_def gcd_non_0_nat)
1.1151 +qed
1.1152 +
1.1153 +(* TODO: definition of index ("discrete logarithm") *)
1.1154 +
1.1155 +end
1.1156 \ No newline at end of file
`