Theory Gaussian_Integers_Sums_Of_Two_Squares

  File:     Gaussian_Integers_Sums_Of_Two_Squares.thy
  Author:   Manuel Eberl, TU München

  Application of Gaussian integers to determining which natural numbers can be written as a sum
  of two squares
subsection ‹Sums of two squares›
theory Gaussian_Integers_Sums_Of_Two_Squares
  imports Gaussian_Integers

text ‹
  As an application, we can now easily prove that a positive natural number is the
  sum of two squares if and only if all prime factors congruent 3 modulo 4 have even

inductive sum_of_2_squares_nat :: "nat  bool" where
  "sum_of_2_squares_nat (a ^ 2 + b ^ 2)"

lemma sum_of_2_squares_nat_altdef: "sum_of_2_squares_nat n  n  range gauss_int_norm"
proof (safe elim!: sum_of_2_squares_nat.cases)
  fix a b :: nat
  have "a ^ 2 + b ^ 2 = gauss_int_norm (of_nat a + 𝗂 * of_nat b)"
    by (auto simp: gauss_int_norm_def nat_add_distrib nat_power_eq)
  thus "a ^ 2 + b ^ 2  range gauss_int_norm" by blast
  fix z :: gauss_int
  have "gauss_int_norm z = nat ¦ReZ z¦ ^ 2 + nat ¦ImZ z¦ ^ 2"
    by (auto simp: gauss_int_norm_def nat_add_distrib simp flip: nat_power_eq)
  thus "sum_of_2_squares_nat (gauss_int_norm z)"
    by (auto intro: sum_of_2_squares_nat.intros)

lemma sum_of_2_squares_nat_gauss_int_norm [intro]: "sum_of_2_squares_nat (gauss_int_norm z)"
  by (auto simp: sum_of_2_squares_nat_altdef)

lemma sum_of_2_squares_nat_0 [simp, intro]: "sum_of_2_squares_nat 0" 
  and sum_of_2_squares_nat_1 [simp, intro]: "sum_of_2_squares_nat 1"
  and sum_of_2_squares_nat_Suc_0 [simp, intro]: "sum_of_2_squares_nat (Suc 0)"
  and sum_of_2_squares_nat_2 [simp, intro]: "sum_of_2_squares_nat 2"
  using sum_of_2_squares_nat.intros[of 0 0] sum_of_2_squares_nat.intros[of 0 1]
        sum_of_2_squares_nat.intros[of 1 1] by (simp_all add: numeral_2_eq_2)

lemma sum_of_2_squares_nat_mult [intro]:
  assumes "sum_of_2_squares_nat x" "sum_of_2_squares_nat y"
  shows   "sum_of_2_squares_nat (x * y)"
proof -
  from assms obtain z1 z2 where "x = gauss_int_norm z1" "y = gauss_int_norm z2"
    by (auto simp: sum_of_2_squares_nat_altdef)
  hence "x * y = gauss_int_norm (z1 * z2)"
    by (simp add: gauss_int_norm_mult)
  thus ?thesis by auto

lemma sum_of_2_squares_nat_power [intro]:
  assumes "sum_of_2_squares_nat m"
  shows   "sum_of_2_squares_nat (m ^ n)"
  using assms by (induction n) auto

lemma sum_of_2_squares_nat_prod [intro]:
  assumes "x. x  A  sum_of_2_squares_nat (f x)"
  shows   "sum_of_2_squares_nat (xA. f x)"
  using assms by (induction A rule: infinite_finite_induct) auto

lemma sum_of_2_squares_nat_prod_mset [intro]:
  assumes "x. x ∈# A  sum_of_2_squares_nat x"
  shows   "sum_of_2_squares_nat (prod_mset A)"
  using assms by (induction A) auto

lemma sum_of_2_squares_nat_necessary:
  assumes "sum_of_2_squares_nat n" "n > 0"
  assumes "prime p" "[p = 3] (mod 4)"
  shows   "even (multiplicity p n)"
proof -
  define k where "k = multiplicity p n"
  from assms obtain z where z: "gauss_int_norm z = n"
    by (auto simp: sum_of_2_squares_nat_altdef)
  from assms and z have [simp]: "z  0"
    by auto
  have prime': "prime (of_nat p :: gauss_int)"
    using assms prime_gauss_int_of_nat by blast
  have [simp]: "multiplicity (of_nat p) (gauss_cnj z) = multiplicity (of_nat p) z"
    using multiplicity_gauss_cnj[of "of_nat p" z] by simp
  have "multiplicity (of_nat p) (of_nat n :: gauss_int) =
        multiplicity (of_nat p) (z * gauss_cnj z)"
    using z by (simp add: self_mult_gauss_cnj)
  also have " = 2 * multiplicity (of_nat p) z"
    using prime' by (subst prime_elem_multiplicity_mult_distrib) auto
  finally have "multiplicity p n = 2 * multiplicity (of_nat p) z"
    by (subst (asm) multiplicity_gauss_int_of_nat)
  thus ?thesis by auto

lemma sum_of_2_squares_nat_sufficient:
  fixes n :: nat
  assumes "n > 0"
  assumes "p. p  prime_factors n  [p = 3] (mod 4)  even (multiplicity p n)"
  shows "sum_of_2_squares_nat n"
proof -
  define P2 where "P2 = {pprime_factors n. [p = 1] (mod 4)}"
  define P3 where "P3 = {pprime_factors n. [p = 3] (mod 4)}"
  from n > 0 have "n = (pprime_factors n. p ^ multiplicity p n)"
    by (subst prime_factorization_nat) auto
  also have " = (p{2}P2P3. p ^ multiplicity p n)"
    using prime_mod_4_cases
    by (intro prod.mono_neutral_left)
       (auto simp: P2_def P3_def in_prime_factors_iff not_dvd_imp_multiplicity_0)
  also have " = (p{2}P2. p ^ multiplicity p n) * (pP3. p ^ multiplicity p n)"
    by (intro prod.union_disjoint) (auto simp: P2_def P3_def cong_def)
  also have "(p{2}P2. p ^ multiplicity p n) =
               2 ^ multiplicity 2 n * (pP2. p ^ multiplicity p n)"
    by (subst prod.union_disjoint) (auto simp: P2_def cong_def)
  also have "(pP3. p ^ multiplicity p n) = (pP3. (p ^ 2) ^ (multiplicity p n div 2))"
  proof (intro prod.cong refl)
    fix p :: nat assume p: "p  P3"
    have "(p ^ 2) ^ (multiplicity p n div 2) = p ^ (2 * (multiplicity p n div 2))"
      by (simp add: power_mult)
    also have "even (multiplicity p n)"
      using assms p by (auto simp: P3_def)
    hence "2 * (multiplicity p n div 2) = multiplicity p n"
      by simp
    finally show "p ^ multiplicity p n = (p ^ 2) ^ (multiplicity p n div 2)"
      by simp
  finally have "n = 2 ^ multiplicity 2 n * (pP2. p ^ multiplicity p n) * 
                      (pP3. p2 ^ (multiplicity p n div 2))" .

  also have "sum_of_2_squares_nat "
  proof (intro sum_of_2_squares_nat_mult sum_of_2_squares_nat_prod; rule sum_of_2_squares_nat_power)
    fix p :: nat assume p: "p  P2"
    with prime_cong_1_mod_4_gauss_int_norm_exists[of p] show "sum_of_2_squares_nat p"
      by (auto simp: P2_def)
    fix p :: nat assume p: "p  P3"
    have "sum_of_2_squares_nat (gauss_int_norm (of_nat p))" ..
    also have "gauss_int_norm (of_nat p) = p ^ 2"
      by simp
    finally show "sum_of_2_squares_nat (p ^ 2)" .
  qed auto
  finally show ?thesis .

theorem sum_of_2_squares_nat_iff:
  "sum_of_2_squares_nat n 
     n = 0  (pprime_factors n. [p = 3] (mod 4)  even (multiplicity p n))"
  using sum_of_2_squares_nat_necessary[of n] sum_of_2_squares_nat_sufficient[of n] by auto