Theory Carmichael_Numbers
section ‹Carmichael Numbers›
theory Carmichael_Numbers
imports
Residues_Nat
begin
text ‹
A Carmichael number is a composite number ‹n› that Fermat's test incorrectly labels
as primes no matter which witness ‹a› is chosen (except in the case that ‹a› shares a
factor with ‹n›). \<^cite>‹"Carmichael_numbers" and "wiki:Carmichael_number"›
›
definition Carmichael_number :: "nat ⇒ bool" where
"Carmichael_number n ⟷ n > 1 ∧ ¬prime n ∧ (∀a. coprime a n ⟶ [a ^ (n - 1) = 1] (mod n))"
lemma Carmichael_number_0[simp, intro]: "¬Carmichael_number 0"
unfolding Carmichael_number_def by simp
lemma Carmichael_number_1[simp, intro]: "¬Carmichael_number 1"
by (auto simp: Carmichael_number_def)
lemma Carmichael_number_Suc_0[simp, intro]: "¬Carmichael_number (Suc 0)"
by (auto simp: Carmichael_number_def)
lemma Carmichael_number_not_prime: "Carmichael_number n ⟹ ¬prime n"
by (auto simp: Carmichael_number_def)
lemma Carmichael_number_gt_3: "Carmichael_number n ⟹ n > 3"
proof -
assume *: "Carmichael_number n"
hence "n > 1" by (auto simp: Carmichael_number_def)
{
assume "¬(n > 3)"
with ‹n > 1› have "n = 2 ∨ n = 3" by auto
with * and Carmichael_number_not_prime[of n] have False by auto
}
thus "n > 3" by auto
qed
text ‹
The proofs are inspired by \<^cite>‹"Carmichael_numbers" and "Carmichael_number_square_free"›.
›
lemma Carmichael_number_imp_squarefree_aux:
assumes "Carmichael_number n"
assumes n: "n = p^r * l" and "prime p" "¬p dvd l"
assumes "r > 1"
shows False
proof -
have "¬ prime n" using ‹Carmichael_number n› unfolding Carmichael_number_def by blast
have * : "[a^(n-1) = 1] (mod n)" if "coprime a n" for a
using ‹Carmichael_number n› that
unfolding Carmichael_number_def
by blast
have "1 ≤ n"
unfolding n using ‹prime p› ‹¬ p dvd l›
by (auto intro: gre1I_nat)
have "2 ≤ n"
proof(cases "n = 1")
case True
then show ?thesis
unfolding n using ‹1 < r› prime_gt_1_nat[OF ‹prime p›]
by simp
next
case False
then show ?thesis using ‹1 ≤ n› by linarith
qed
have "p < p^r"
using prime_gt_1_nat[OF ‹prime p›] ‹1 < r›
by (metis power_one_right power_strict_increasing_iff)
hence "p < n" using ‹1 ≤ n› less_le_trans n by fastforce
then have [simp]: "{..n} - {0..Suc 0} = {2..n}" by auto
obtain a where a: "[a = p + 1] (mod p^r)" "[a = 1] (mod l)"
using binary_chinese_remainder_nat[of "p^r" l "p + 1" 1]
and ‹prime p› prime_imp_coprime_nat coprime_power_left_iff ‹¬p dvd l›
by blast
hence "coprime a n"
using lucas_coprime_lemma[of 1 a l] cong_imp_coprime[of "p+1" a "p^r"]
and coprime_add_one_left cong_sym
unfolding ‹n = p ^ r * l› coprime_mult_right_iff coprime_power_right_iff power_one_right
by blast
hence "[a ^ (n - 1) = 1] (mod n)"
using * by blast
hence "[a ^ (n - 1) = 1] (mod p^r)"
using n cong_modulus_mult_nat by blast
hence A: "[a ^ n = a] (mod p^r)"
using cong_scalar_right[of "a^(n-1)" 1 "p^r" a] ‹1 ≤ n›
unfolding power_Suc2[symmetric]
by simp
have "r = Suc (Suc (r - 2))"
using ‹1 < r› by linarith
then have "p^r = p^2 * p^(r-2)"
by (simp add: algebra_simps flip: power_add power_Suc)
hence "[a ^ n = a] (mod p^2)" "[a = p + 1] (mod p^2)"
using ‹1 < r› A cong_modulus_mult_nat ‹[a = p + 1] (mod p^r)›
by algebra+
hence 1: "[(p + 1) ^ n = (p + 1)] (mod p^2)"
by (metis (mono_tags) cong_def power_mod)
have "[(p + 1) ^ n = (∑k≤n. of_nat (n choose k) * p ^ k * 1 ^ (n - k))] (mod p^2)"
using binomial[of p 1 n] by simp
also have "(∑k≤n. of_nat (n choose k) * p ^ k * 1 ^ (n - k)) =
(∑k = 0..1. (n choose k) * p ^ k) + (∑k∈ {2..n}. of_nat (n choose k) * p ^ k * 1 ^ (n - k))"
using ‹2 ≤ n› finite_atMost[of n]
by (subst sum.subset_diff[where B = "{0..1}"]) auto
also have "[(∑k = 0..1. (n choose k) * p ^ k) = 1] (mod p^2)"
by (simp add: cong_altdef_nat ‹p ^ r = p⇧2 * p ^ (r - 2)› n)
also have "[(∑k∈ {2..n}. of_nat (n choose k) * p ^ k * 1 ^ (n - k)) = 0] (mod p^2)"
by (rule cong_eq_0_I) (clarsimp simp: cong_0_iff le_imp_power_dvd)
finally have 2: "[(p + 1) ^ n = 1] (mod p^2)" by simp
from cong_trans[OF cong_sym[OF 1] 2]
show ?thesis
using prime_gt_1_nat[OF ‹prime p›]
by (auto dest: residue_one_dvd[unfolded One_nat_def] simp add: cong_def numeral_2_eq_2)
qed
theorem Carmichael_number_imp_squarefree:
assumes "Carmichael_number n"
shows "squarefree n"
proof(rule squarefreeI, rule ccontr)
fix x :: nat
assume "x⇧2 dvd n"
from assms have "n > 0" using Carmichael_number_gt_3[of n] by auto
from ‹x⇧2 dvd n› and ‹0 < n› have "0 < x" by auto
assume "¬ is_unit x"
then obtain p where "prime p" "p dvd x"
using prime_divisor_exists[of x] ‹0 < x›
by blast
with ‹x⇧2 dvd n› have "p^2 dvd n"
by auto
obtain l where n: "n = p ^ multiplicity p n * l"
using multiplicity_dvd[of p n] by blast
then have "¬ p dvd l"
using multiplicity_decompose'[where x = n and p = p]
using ‹prime p› ‹0 < n›
by (metis nat_dvd_1_iff_1 nat_mult_eq_cancel1 neq0_conv prime_prime_factor_sqrt zero_less_power)
have "2 ≤ multiplicity p n"
using ‹p⇧2 dvd n› ‹0 < n› prime_gt_1_nat[OF ‹prime p›]
by (auto intro!: multiplicity_geI simp: power2_eq_square)
then show False
using Carmichael_number_imp_squarefree_aux[OF ‹Carmichael_number n› n] ‹prime p› ‹¬ p dvd l›
by auto
qed
corollary Carmichael_not_primepow:
assumes "Carmichael_number n"
shows "¬primepow n"
using Carmichael_number_imp_squarefree[of n] Carmichael_number_not_prime[of n] assms
primepow_gt_0_nat[of n] by (auto simp: not_squarefree_primepow)
lemma Carmichael_number_imp_squarefree_alt_weak:
assumes "Carmichael_number n"
shows "∃p l. (n = p * l) ∧ prime p ∧ ¬p dvd l"
proof -
from assms have "n > 1"
using Carmichael_number_gt_3[of n] by simp
have "squarefree n"
using Carmichael_number_imp_squarefree assms
by blast
obtain p l where "p * l = n" "prime p" "1 < p"
using assms prime_divisor_exists_strong_nat prime_gt_1_nat
unfolding Carmichael_number_def by blast
then have "multiplicity p n = 1"
using ‹1 < n› ‹squarefree n› and multiplicity_eq_zero_iff[of n p] squarefree_factorial_semiring''[of n]
by auto
then have "¬p dvd l"
using ‹1 < n› ‹prime p› ‹p * l = n› multiplicity_decompose'[of n p]
by force
show ?thesis
using ‹p * l = n› ‹prime p› ‹¬p dvd l›
by blast
qed
theorem Carmichael_number_odd:
assumes "Carmichael_number n"
shows "odd n"
proof (rule ccontr)
assume "¬ odd n"
hence "even n" by simp
from assms have "n ≥ 4" using Carmichael_number_gt_3[of n] by simp
have "[(n - 1) ^ (n - 1) = n - 1] (mod n)"
using ‹even n› and ‹n ≥ 4› by (intro odd_pow_cong) auto
then have "[(n - 1) ^ (n - 1) ≠ 1] (mod n)"
using cong_trans[of 1 "(n - 1) ^ (n - 1)" n "n-1", OF cong_sym] ‹4 ≤ n›
by (auto simp: cong_def)
moreover have "coprime (n - 1) n"
using ‹n ≥ 4› coprime_diff_one_left_nat[of n] by auto
ultimately show False
using assms unfolding Carmichael_number_def by blast
qed
lemma Carmichael_number_imp_squarefree_alt:
assumes "Carmichael_number n"
shows "∃p l. (n = p * l) ∧ prime p ∧ ¬p dvd l ∧ 2 < l"
proof -
obtain p l where [simp]: "(n = p * l)" and "prime p" "¬p dvd l"
using Carmichael_number_imp_squarefree_alt_weak and assms by blast
moreover have "odd n" using Carmichael_number_odd and assms by blast
consider "l = 0 ∨ l = 2" | "l = 1" | "2 < l"
by fastforce
then have "2 < l"
proof cases
case 1
then show ?thesis
using ‹odd n› by auto
next
case 2
then show ?thesis
using ‹n = p * l› ‹prime p› ‹Carmichael_number n›
unfolding Carmichael_number_def by simp
qed simp
ultimately show ?thesis by blast
qed
lemma Carmichael_number_imp_dvd:
fixes n :: nat
assumes Carmichael_number: "Carmichael_number n" and "prime p" "p dvd n"
shows "p - 1 dvd n - 1"
proof -
have "¬prime n" using Carmichael_number unfolding Carmichael_number_def by blast
obtain u where "n = p * u" using ‹p dvd n› by blast
have "squarefree n" using Carmichael_number_imp_squarefree assms by blast
then have "¬p dvd u"
using ‹prime p› not_prime_unit[of p]
unfolding power2_eq_square squarefree_def ‹n = p * u›
by fastforce
define R where "R = Residues_nat p"
interpret residues_nat_prime p R
by unfold_locales (simp_all only: ‹prime p› R_def)
obtain a where a: "a ∈ {0<..<p}" "units.ord a = p - 1"
using residues_prime_cyclic' ‹prime p› by metis
from a have "a ∈ totatives p" by (auto simp: totatives_prime ‹prime p›)
have "coprime p u"
using ‹prime p› ‹¬ p dvd u›
by (simp add: prime_imp_coprime_nat)
then obtain x where "[x = a] (mod p)" "[x = 1] (mod u)"
using binary_chinese_remainder_nat[of p u a 1] by blast
have "coprime x p"
using ‹a ∈ totatives p› and cong_imp_coprime[OF cong_sym[OF ‹[x = a] (mod p)›]]
by (simp add: coprime_commute totatives_def)
moreover have "coprime x u"
using coprime_1_left and cong_imp_coprime[OF cong_sym[OF ‹[x = 1] (mod u)›]] by blast
ultimately have "coprime x n"
by (simp add: ‹n = p * u›)
have "[a ^ (n - 1) = x ^ (n - 1)] (mod p)"
using ‹[x = a] (mod p)› by (intro cong_pow) (auto simp: cong_sym_eq)
also have "[x ^ (n - 1) = 1] (mod n)"
using Carmichael_number ‹coprime x n› unfolding Carmichael_number_def by blast
then have "[x ^ (n - 1) = 1] (mod p)"
using ‹n = p * u› cong_modulus_mult_nat by blast
finally have "ord p a dvd n - 1"
by (simp add: ord_divides [symmetric])
also have "ord p a = p - 1"
using a ‹a ∈ totatives p› by (simp add: units.ord_residue_mult_group)
finally show ?thesis .
qed
text ‹
The following lemma is also called Korselt's criterion.
›
lemma Carmichael_numberI:
fixes n :: nat
assumes "¬ prime n" "squarefree n" "1 < n" and
DIV: "⋀p. p ∈ prime_factors n ⟹ p - 1 dvd n - 1"
shows "Carmichael_number n"
unfolding Carmichael_number_def
proof (intro assms conjI allI impI)
fix a :: nat assume "coprime a n"
have n: "n = ∏(prime_factors n)"
using prime_factorization_nat and squarefree_factorial_semiring'[of n] ‹1 < n› ‹squarefree n›
by fastforce
have "x ∈# prime_factorization n ⟹ y ∈# prime_factorization n ⟹ x ≠ y ⟹ coprime x y" for x y
using in_prime_factors_imp_prime primes_coprime
by blast
moreover {
fix p
assume p: "p ∈# prime_factorization n"
have "¬p dvd a"
using ‹coprime a n› p coprime_common_divisor_nat[of a n p]
by (auto simp: in_prime_factors_iff)
with p have "[a ^ (p - 1) = 1] (mod p)"
by (intro fermat_theorem) auto
hence "ord p a dvd p - 1"
by (subst (asm) ord_divides)
also from p have "p - 1 dvd n - 1"
by (rule DIV)
finally have "[a ^ (n - 1) = 1] (mod p)"
by (subst ord_divides)
}
ultimately show "[a ^ (n - 1) = 1] (mod n)"
using n coprime_cong_prod_nat by metis
qed
theorem Carmichael_number_iff:
"Carmichael_number n ⟷
n ≠ 1 ∧ ¬prime n ∧ squarefree n ∧ (∀p∈prime_factors n. p - 1 dvd n - 1)"
proof -
consider "n = 0" | "n = 1" | "n > 1" by force
thus ?thesis using Carmichael_numberI[of n] Carmichael_number_imp_dvd[of n]
by cases (auto simp: Carmichael_number_not_prime Carmichael_number_imp_squarefree)
qed
text ‹
Every Carmichael number has at least three distinct prime factors.
›
theorem Carmichael_number_card_prime_factors:
assumes "Carmichael_number n"
shows "card (prime_factors n) ≥ 3"
proof (rule ccontr)
from assms have "n > 3"
using Carmichael_number_gt_3[of n] by simp
assume "¬(card (prime_factors n) ≥ 3)"
moreover have "card (prime_factors n) ≠ 0"
using assms Carmichael_number_gt_3[of n] by (auto simp: prime_factorization_empty_iff)
moreover have "card (prime_factors n) ≠ 1"
using assms by (auto simp: one_prime_factor_iff_primepow Carmichael_not_primepow)
ultimately have "card (prime_factors n) = 2"
by linarith
then obtain p q where pq: "prime_factors n = {p, q}" "p ≠ q"
by (auto simp: card_Suc_eq numeral_2_eq_2)
hence "prime p" "prime q" by (auto simp: in_prime_factors_iff)
have "n = ∏(prime_factors n)"
using assms by (subst squarefree_imp_prod_prime_factors_eq)
(auto simp: Carmichael_number_imp_squarefree)
with pq have n_eq: "n = p * q" by simp
have "p - 1 dvd n - 1" and "q - 1 dvd n - 1" using assms pq
unfolding Carmichael_number_iff by blast+
with ‹prime p› ‹prime q› ‹n = p * q› ‹p ≠ q› show False
proof (induction p q rule: linorder_wlog)
case (le p q)
hence "p < q" by auto
have "[q = 1] (mod q - 1)"
using prime_gt_1_nat[of q] ‹prime q› by (simp add: cong_def le_mod_geq)
hence "[p * q - 1 = p * 1 - 1] (mod q - 1)"
using le prime_gt_1_nat[of p] by (intro cong_diff_nat cong_mult) auto
hence "[p - 1 = n - 1] (mod q - 1)"
by (simp add: ‹n = p * q› cong_sym_eq)
also have "[n - 1 = 0] (mod q - 1)"
using le by (simp add: cong_def)
finally have "(p - 1) mod (q - 1) = 0"
by (simp add: cong_def)
also have "(p - 1) mod (q - 1) = p - 1"
using prime_gt_1_nat[of p] ‹prime p› ‹p < q› by (intro mod_less) auto
finally show False
using prime_gt_1_nat[of p] ‹prime p› by simp
qed (simp_all add: mult.commute)
qed
lemma Carmichael_number_iff':
fixes n :: nat
defines "P ≡ prime_factorization n"
shows "Carmichael_number n ⟷
n > 1 ∧ size P ≠ 1 ∧ (∀p∈#P. count P p = 1 ∧ p - 1 dvd n - 1)"
unfolding Carmichael_number_iff
by (cases "n = 0") (auto simp: P_def squarefree_factorial_semiring' count_prime_factorization)
text ‹
The smallest Carmichael number is 561, and it was found and proven so by
Carmichael in 1910~\<^cite>‹"carmichael1910note"›.
›
lemma Carmichael_number_561: "Carmichael_number 561" (is "Carmichael_number ?n")
proof -
have [simp]: "prime_factorization (561 :: nat) = {#3, 11, 17#}"
by (rule prime_factorization_eqI) auto
show ?thesis by (subst Carmichael_number_iff') auto
qed
end