open scoped BigOperators def CK : ℕ := 3942951359960012586542991835686376608231592127249807732373409846031135195659174148737161255930050543559319182152642816343958573976075461198274610155058226350701077796608546283231637018483208223116080559321429158623772466374556290759164277947630417236158147995116126734474452247965418364460529839644657 def CG : ℕ := 3942951359960012586542991835686376608231592127249807732373409846031135195659174148737161255930050543559319182152642816343958573976075461198274610155058226350701077796608546283231637018483208223116080561800334422176622099740983337736621316898600121619871377542107047343253864459964167331555646795960321 def CD : ℕ := 45592577 def CQ : ℕ := 487824887233 def CP (n : ℕ) : ℕ := CD * ∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i def CL (j : ℕ) : ℕ := 12 * (j + 1) def CA (j : ℕ) : ℕ := CK * CP (CL j) lemma CD_mul_CG : CD * CG = Nat.fermatNumber 10 := by change CD * CG = 2 ^ 1024 + 1 rw [show 1024 = 128 * 8 by norm_num, pow_mul] norm_num [CD, CG] lemma CP_mul_CG {n : ℕ} (hn : 10 < n) : CP n * CG = 2 ^ (2 ^ n) - 1 := by have h10 : 10 ∈ Finset.range n := Finset.mem_range.mpr hn calc CP n * CG = (∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i) * (CD * CG) := by simp [CP] ring _ = (∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i) * Nat.fermatNumber 10 := by rw [CD_mul_CG] _ = ∏ i ∈ Finset.range n, Nat.fermatNumber i := Finset.prod_erase_mul (Finset.range n) Nat.fermatNumber h10 _ = Nat.fermatNumber n - 2 := Nat.prod_fermatNumber n _ = 2 ^ (2 ^ n) - 1 := by simp [Nat.fermatNumber] lemma CP_pos (n : ℕ) : 0 < CP n := by apply Nat.mul_pos · norm_num [CD] · rw [CanonicallyOrderedAdd.prod_pos] intro i hi simp [Nat.fermatNumber] lemma CL_gt_ten (j : ℕ) : 10 < CL j := by simp [CL] omega lemma CP_mul_CG_add_one {n : ℕ} (hn : 10 < n) : CP n * CG + 1 = 2 ^ (2 ^ n) := by rw [CP_mul_CG hn] have hx : 0 < 2 ^ (2 ^ n) := by positivity omega lemma CA_lt_power (j : ℕ) : CA j < 2 ^ (2 ^ CL j) := by have hp := CP_pos (CL j) have hkg : CK < CG := by norm_num [CK, CG] have hm := Nat.mul_lt_mul_of_pos_right hkg hp calc CA j = CK * CP (CL j) := rfl _ < CG * CP (CL j) := hm _ = CP (CL j) * CG := by ring _ = 2 ^ (2 ^ CL j) - 1 := CP_mul_CG (CL_gt_ten j) _ < 2 ^ (2 ^ CL j) := by have hx : 0 < 2 ^ (2 ^ CL j) := by positivity omega lemma CA_ratio_lower (j : ℕ) : 3 * (2 ^ (2 ^ CL j) - 1) < 4 * CA j := by have hp := CP_pos (CL j) have hratio : 3 * CG < 4 * CK := by norm_num [CK, CG] have hm := Nat.mul_lt_mul_of_pos_right hratio hp have hpg := CP_mul_CG (CL_gt_ten j) calc 3 * (2 ^ (2 ^ CL j) - 1) = 3 * (CP (CL j) * CG) := by rw [hpg] _ = (3 * CG) * CP (CL j) := by ring _ < (4 * CK) * CP (CL j) := hm _ = 4 * CA j := by simp only [CA]; ring lemma CL_ge_twelve (j : ℕ) : 12 ≤ CL j := by simp [CL] lemma exponent_ge_forty_one (j : ℕ) : 41 ≤ 2 ^ CL j := by have h := Nat.pow_le_pow_right (by norm_num : 0 < 2) (CL_ge_twelve j) norm_num at h ⊢ omega lemma power_large (j : ℕ) : 4 * CQ + 3 < 2 ^ (2 ^ CL j) := by have hbase : 4 * CQ + 3 < 2 ^ 41 := by norm_num [CQ] exact lt_of_lt_of_le hbase (Nat.pow_le_pow_right (by norm_num : 0 < 2) (exponent_ge_forty_one j)) lemma CA_ne_cover_prime (j a q : ℕ) (hqpos : 0 < q) (hqle : q ≤ CQ) : CA j ≠ q + 2 ^ a := by intro heq have htermA : 2 ^ a < CA j := by omega have htermX : 2 ^ a < 2 ^ (2 ^ CL j) := lt_trans htermA (CA_lt_power j) have ha : a < 2 ^ CL j := (Nat.pow_lt_pow_iff_right (by norm_num : 1 < 2)).mp htermX have hdouble : 2 * 2 ^ a ≤ 2 ^ (2 ^ CL j) := by calc 2 * 2 ^ a = 2 ^ (a + 1) := by rw [pow_succ]; ring _ ≤ 2 ^ (2 ^ CL j) := Nat.pow_le_pow_right (by norm_num : 0 < 2) (by omega) have hlow := CA_ratio_lower j have hlarge := power_large j rw [heq] at hlow omega lemma outer_power_rewrite (j : ℕ) : 2 ^ (2 ^ CL j) = (2 ^ 4096) ^ (4096 ^ j) := by calc 2 ^ (2 ^ CL j) = 2 ^ ((2 ^ 12) ^ (j + 1)) := by rw [CL, pow_mul] _ = 2 ^ (4096 ^ (j + 1)) := by norm_num _ = 2 ^ (4096 * 4096 ^ j) := by congr 1 rw [pow_succ] ring _ = (2 ^ 4096) ^ (4096 ^ j) := by rw [pow_mul] lemma stable_iter {q u : ℕ} (h : u ^ 4096 ≡ u [MOD q]) : ∀ j : ℕ, u ^ (4096 ^ j) ≡ u [MOD q] := by intro j induction j with | zero => simpa using (Nat.ModEq.refl u : u ≡ u [MOD q]) | succ j ih => rw [pow_succ, pow_mul] exact (ih.pow 4096).trans h lemma two_pow_mod_period {n m r q : ℕ} (hr : n % m = r) (hperiod : 2 ^ m ≡ 1 [MOD q]) : 2 ^ n ≡ 2 ^ r [MOD q] := by have hdecomp : m * (n / m) + r = n := by rw [← hr] exact Nat.div_add_mod n m calc 2 ^ n = 2 ^ (m * (n / m) + r) := by rw [hdecomp] _ = (2 ^ m) ^ (n / m) * 2 ^ r := by rw [pow_add, pow_mul] _ ≡ 1 ^ (n / m) * 2 ^ r [MOD q] := (hperiod.pow (n / m)).mul (Nat.ModEq.refl (2 ^ r)) _ = 2 ^ r := by simp abbrev CoverCert (m r q u : ℕ) : Prop := 0 < q ∧ q ≤ CQ ∧ q ≠ 1 ∧ Nat.gcd q CG = 1 ∧ 1 ≤ u ∧ 2 ^ m ≡ 1 [MOD q] ∧ 2 ^ (4096 % m) ≡ u [MOD q] ∧ (4096 * 4096) % m = 4096 % m ∧ CK * (u - 1) ≡ CG * 2 ^ r [MOD q] lemma one_power_case (j a p m r q u : ℕ) (ha : a % m = r) (hp : p.Prime) (heq : CA j = p + 2 ^ a) (hc : CoverCert m r q u) : False := by rcases hc with ⟨hqpos, hqle, hqone, hcop, huone, hperiod, husmall, hcycle, hbase⟩ have hu : 2 ^ 4096 ≡ u [MOD q] := (two_pow_mod_period (rfl : 4096 % m = 4096 % m) hperiod).trans husmall have hstable : u ^ 4096 ≡ u [MOD q] := by calc u ^ 4096 ≡ (2 ^ 4096) ^ 4096 [MOD q] := (hu.pow 4096).symm _ = 2 ^ (4096 * 4096) := by rw [pow_mul] _ ≡ 2 ^ (4096 % m) [MOD q] := two_pow_mod_period hcycle hperiod _ ≡ u [MOD q] := husmall have hXU : 2 ^ (2 ^ CL j) ≡ u [MOD q] := by rw [outer_power_rewrite] exact (hu.pow (4096 ^ j)).trans (stable_iter hstable j) have hXone : 1 ≤ 2 ^ (2 ^ CL j) := by have hx : 0 < 2 ^ (2 ^ CL j) := by positivity omega have hXm1 : 2 ^ (2 ^ CL j) - 1 ≡ u - 1 [MOD q] := hXU.sub hXone huone (Nat.ModEq.refl 1) have hGA : CG * CA j ≡ CG * 2 ^ r [MOD q] := by calc CG * CA j = CK * (CP (CL j) * CG) := by simp only [CA] ring _ = CK * (2 ^ (2 ^ CL j) - 1) := by rw [CP_mul_CG (CL_gt_ten j)] _ ≡ CK * (u - 1) [MOD q] := hXm1.mul_left CK _ ≡ CG * 2 ^ r [MOD q] := hbase have hA : CA j ≡ 2 ^ r [MOD q] := hGA.cancel_left_of_coprime hcop have hpow : 2 ^ a ≡ 2 ^ r [MOD q] := two_pow_mod_period ha hperiod have hrepr : p + 2 ^ a ≡ 2 ^ r [MOD q] := by rw [← heq] exact hA have hpr : p + 2 ^ r ≡ 2 ^ r [MOD q] := ((Nat.ModEq.refl p).add hpow).symm.trans hrepr have hpzero : p ≡ 0 [MOD q] := by apply Nat.ModEq.add_right_cancel' (2 ^ r) simpa using hpr have hdiv : q ∣ p := Nat.modEq_zero_iff_dvd.mp hpzero rcases (Nat.dvd_prime hp).mp hdiv with hq | hq · exact hqone hq · exact CA_ne_cover_prime j a q hqpos hqle (by simpa [hq] using heq) lemma cover_cert_3_0_7 : CoverCert 3 0 7 2 := by norm_num [CoverCert, Nat.ModEq, CK, CG, CQ] lemma cover_cert_5_0_31 : CoverCert 5 0 31 2 := by decide lemma cover_cert_9_1_73 : CoverCert 9 1 73 2 := by decide lemma cover_cert_10_1_11 : CoverCert 10 1 11 9 := by decide lemma cover_cert_12_8_13 : CoverCert 12 8 13 3 := by decide lemma cover_cert_15_8_151 : CoverCert 15 8 151 2 := by decide lemma cover_cert_18_4_19 : CoverCert 18 4 19 17 := by decide lemma cover_cert_20_7_41 : CoverCert 20 7 41 18 := by decide lemma cover_cert_24_5_241 : CoverCert 24 5 241 225 := by decide lemma cover_cert_30_29_331 : CoverCert 30 29 331 329 := by decide lemma cover_cert_36_2_37 : CoverCert 36 2 37 12 := by decide lemma cover_cert_36_14_109 : CoverCert 36 14 109 66 := by decide lemma cover_cert_40_17_61681 : CoverCert 40 17 61681 3855 := by decide lemma cover_cert_45_34_631 : CoverCert 45 34 631 2 := by decide lemma cover_cert_45_43_23311 : CoverCert 45 43 23311 2 := by decide lemma cover_cert_48_13_97 : CoverCert 48 13 97 61 := by decide lemma cover_cert_48_37_673 : CoverCert 48 37 673 255 := by decide lemma cover_cert_60_16_61 : CoverCert 60 16 61 22 := by decide lemma cover_cert_60_19_1321 : CoverCert 60 19 1321 807 := by decide lemma cover_cert_72_26_433 : CoverCert 72 26 433 296 := by decide lemma cover_cert_72_62_38737 : CoverCert 72 62 38737 11954 := by decide lemma cover_cert_90_52_18837001 : CoverCert 90 52 18837001 18836999 := by decide lemma cover_cert_120_37_4562284561 : CoverCert 120 37 4562284561 65536 := by decide lemma cover_cert_144_49_577 : CoverCert 144 49 577 435 := by decide lemma cover_cert_144_121_487824887233 : CoverCert 144 121 487824887233 123861787774 := by decide lemma cover_cert_180_103_181 : CoverCert 180 103 181 38 := by decide lemma cover_cert_180_106_54001 : CoverCert 180 106 54001 17097 := by decide lemma cover_cert_360_229_168692292721 : CoverCert 360 229 168692292721 140414064110 := by decide abbrev Covered (x : ℕ) : Prop := x % 3 = 0 ∨ x % 5 = 0 ∨ x % 9 = 1 ∨ x % 10 = 1 ∨ x % 12 = 8 ∨ x % 15 = 8 ∨ x % 18 = 4 ∨ x % 20 = 7 ∨ x % 24 = 5 ∨ x % 30 = 29 ∨ x % 36 = 2 ∨ x % 36 = 14 ∨ x % 40 = 17 ∨ x % 45 = 34 ∨ x % 45 = 43 ∨ x % 48 = 13 ∨ x % 48 = 37 ∨ x % 60 = 16 ∨ x % 60 = 19 ∨ x % 72 = 26 ∨ x % 72 = 62 ∨ x % 90 = 52 ∨ x % 120 = 37 ∨ x % 144 = 49 ∨ x % 144 = 121 ∨ x % 180 = 103 ∨ x % 180 = 106 ∨ x % 360 = 229 lemma cover_grid : ∀ i : Fin 24, ∀ j : Fin 30, Covered (30 * i.val + j.val) := by decide lemma cover_system (a : ℕ) : Covered a := by let x := a % 720 have hi : x / 30 < 24 := by dsimp [x] omega have hj : x % 30 < 30 := Nat.mod_lt _ (by norm_num) have h := cover_grid ⟨x / 30, hi⟩ ⟨x % 30, hj⟩ have heq : 30 * (x / 30) + x % 30 = x := Nat.div_add_mod x 30 rw [heq] at h dsimp [Covered, x] at h ⊢ norm_num [Nat.mod_mod_of_dvd] at h ⊢ exact h lemma CA_not_prime_plus_power (j a p : ℕ) (hp : p.Prime) : CA j ≠ p + 2 ^ a := by intro heq rcases cover_system a with h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h · exact one_power_case j a p 3 0 7 2 h hp heq cover_cert_3_0_7 · exact one_power_case j a p 5 0 31 2 h hp heq cover_cert_5_0_31 · exact one_power_case j a p 9 1 73 2 h hp heq cover_cert_9_1_73 · exact one_power_case j a p 10 1 11 9 h hp heq cover_cert_10_1_11 · exact one_power_case j a p 12 8 13 3 h hp heq cover_cert_12_8_13 · exact one_power_case j a p 15 8 151 2 h hp heq cover_cert_15_8_151 · exact one_power_case j a p 18 4 19 17 h hp heq cover_cert_18_4_19 · exact one_power_case j a p 20 7 41 18 h hp heq cover_cert_20_7_41 · exact one_power_case j a p 24 5 241 225 h hp heq cover_cert_24_5_241 · exact one_power_case j a p 30 29 331 329 h hp heq cover_cert_30_29_331 · exact one_power_case j a p 36 2 37 12 h hp heq cover_cert_36_2_37 · exact one_power_case j a p 36 14 109 66 h hp heq cover_cert_36_14_109 · exact one_power_case j a p 40 17 61681 3855 h hp heq cover_cert_40_17_61681 · exact one_power_case j a p 45 34 631 2 h hp heq cover_cert_45_34_631 · exact one_power_case j a p 45 43 23311 2 h hp heq cover_cert_45_43_23311 · exact one_power_case j a p 48 13 97 61 h hp heq cover_cert_48_13_97 · exact one_power_case j a p 48 37 673 255 h hp heq cover_cert_48_37_673 · exact one_power_case j a p 60 16 61 22 h hp heq cover_cert_60_16_61 · exact one_power_case j a p 60 19 1321 807 h hp heq cover_cert_60_19_1321 · exact one_power_case j a p 72 26 433 296 h hp heq cover_cert_72_26_433 · exact one_power_case j a p 72 62 38737 11954 h hp heq cover_cert_72_62_38737 · exact one_power_case j a p 90 52 18837001 18836999 h hp heq cover_cert_90_52_18837001 · exact one_power_case j a p 120 37 4562284561 65536 h hp heq cover_cert_120_37_4562284561 · exact one_power_case j a p 144 49 577 435 h hp heq cover_cert_144_49_577 · exact one_power_case j a p 144 121 487824887233 123861787774 h hp heq cover_cert_144_121_487824887233 · exact one_power_case j a p 180 103 181 38 h hp heq cover_cert_180_103_181 · exact one_power_case j a p 180 106 54001 17097 h hp heq cover_cert_180_106_54001 · exact one_power_case j a p 360 229 168692292721 140414064110 h hp heq cover_cert_360_229_168692292721 lemma two_pow_mod_sixteen_zero {a : ℕ} (ha : 4 ≤ a) : 2 ^ a % 16 = 0 := by have hsplit : a = 4 + (a - 4) := by omega rw [hsplit, pow_add] norm_num lemma CA_mod_sixteen (j : ℕ) : CA j % 16 = 15 := by have hfour : 4 ≤ 2 ^ CL j := by exact le_trans (by norm_num) (exponent_ge_forty_one j) have hzero : 2 ^ (2 ^ CL j) ≡ 0 [MOD 16] := by exact two_pow_mod_sixteen_zero hfour have hsixteen : 2 ^ (2 ^ CL j) ≡ 16 [MOD 16] := by exact hzero.trans (by norm_num [Nat.ModEq]) have hpos0 : 0 < 2 ^ (2 ^ CL j) := by positivity have hpos : 1 ≤ 2 ^ (2 ^ CL j) := by omega have hsub : 2 ^ (2 ^ CL j) - 1 ≡ 15 [MOD 16] := by simpa using hsixteen.sub hpos (by norm_num : 1 ≤ 16) (Nat.ModEq.refl 1) have hprod : CP (CL j) * CG ≡ 15 [MOD 16] := by rw [CP_mul_CG (CL_gt_ten j)] exact hsub have hG : CG ≡ 1 [MOD 16] := by norm_num [Nat.ModEq, CG] have hP : CP (CL j) ≡ 15 [MOD 16] := by calc CP (CL j) = CP (CL j) * 1 := by simp _ ≡ CP (CL j) * CG [MOD 16] := ((Nat.ModEq.refl (CP (CL j))).mul hG).symm _ ≡ 15 [MOD 16] := hprod have hK : CK ≡ 1 [MOD 16] := by norm_num [Nat.ModEq, CK] have hA : CA j ≡ 15 [MOD 16] := by calc CA j = CK * CP (CL j) := rfl _ ≡ 1 * 15 [MOD 16] := hK.mul hP _ = 15 := by norm_num exact hA lemma CP_one_lt (n : ℕ) : 1 < CP n := by have hprodpos : 0 < ∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i := by rw [CanonicallyOrderedAdd.prod_pos] intro i hi simp [Nat.fermatNumber] have hprod : 1 ≤ ∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i := by omega calc 1 < CD := by norm_num [CD] _ = CD * 1 := by simp _ ≤ CD * ∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i := Nat.mul_le_mul_left CD hprod _ = CP n := rfl lemma CA_gt_fifteen (j : ℕ) : 15 < CA j := by have hppos : 0 < CP (CL j) := CP_pos _ have hp : 1 ≤ CP (CL j) := by omega calc 15 < CK := by norm_num [CK] _ = CK * 1 := by simp _ ≤ CK * CP (CL j) := Nat.mul_le_mul_left CK hp _ = CA j := rfl lemma CA_not_prime (j : ℕ) : ¬(CA j).Prime := by intro hp have hkdvd : CK ∣ CA j := by refine ⟨CP (CL j), ?_⟩ rfl rcases (Nat.dvd_prime hp).mp hkdvd with hk | hk · norm_num [CK] at hk · have hplt : 1 < CP (CL j) := CP_one_lt _ have hkpos : 0 < CK := by norm_num [CK] have hlt : CK < CA j := by calc CK = CK * 1 := by simp _ < CK * CP (CL j) := Nat.mul_lt_mul_of_pos_left hplt hkpos _ = CA j := rfl omega def BF (r : ℕ) : ℕ := if r = 10 then CD else Nat.fermatNumber r lemma fermatNumber_mod_sixteen {r : ℕ} (hr : 2 ≤ r) : Nat.fermatNumber r % 16 = 1 := by have hfour : 4 ≤ 2 ^ r := by have h := Nat.pow_le_pow_right (by norm_num : 0 < 2) hr norm_num at h ⊢ omega have hz : 2 ^ (2 ^ r) ≡ 0 [MOD 16] := two_pow_mod_sixteen_zero hfour have h : Nat.fermatNumber r ≡ 1 [MOD 16] := by calc Nat.fermatNumber r = 2 ^ (2 ^ r) + 1 := rfl _ ≡ 0 + 1 [MOD 16] := hz.add (Nat.ModEq.refl 1) _ = 1 := by norm_num exact h lemma BF_one_lt (r : ℕ) : 1 < BF r := by unfold BF split_ifs with h · norm_num [CD] · have hF : 2 < Nat.fermatNumber r := Nat.two_lt_fermatNumber r omega lemma BF_residue_class (r : ℕ) : BF r = 3 ∨ BF r = 5 ∨ BF r % 16 = 1 := by by_cases h0 : r = 0 · subst r left norm_num [BF, Nat.fermatNumber] by_cases h1 : r = 1 · subst r right; left norm_num [BF, Nat.fermatNumber] have hr : 2 ≤ r := by omega right; right by_cases h10 : r = 10 · subst r norm_num [BF, CD] · simp only [BF, if_neg h10] exact fermatNumber_mod_sixteen hr lemma two_power_residue_class {p a b : ℕ} (hb : 0 < b) (hba : b < a) (hpclass : p = 3 ∨ p = 5 ∨ p % 16 = 1) (hmod : (p + 2 ^ a + 2 ^ b) % 16 = 15) : (p = 3 ∧ a = 3 ∧ b = 2) ∨ (p = 5 ∧ a = 3 ∧ b = 1) := by rcases lt_or_ge a 4 with ha | ha · have hcases : (a = 2 ∧ b = 1) ∨ (a = 3 ∧ b = 1) ∨ (a = 3 ∧ b = 2) := by omega rcases hcases with h21 | h31 | h32 · rcases h21 with ⟨rfl, rfl⟩ rcases hpclass with rfl | rfl | hpmod · norm_num at hmod · norm_num at hmod · simp [Nat.add_mod, hpmod] at hmod · rcases h31 with ⟨rfl, rfl⟩ rcases hpclass with rfl | rfl | hpmod · norm_num at hmod · exact Or.inr ⟨rfl, rfl, rfl⟩ · simp [Nat.add_mod, hpmod] at hmod · rcases h32 with ⟨rfl, rfl⟩ rcases hpclass with rfl | rfl | hpmod · exact Or.inl ⟨rfl, rfl, rfl⟩ · norm_num at hmod · simp [Nat.add_mod, hpmod] at hmod · have hamod : 2 ^ a % 16 = 0 := two_pow_mod_sixteen_zero ha have hbclass : 2 ^ b % 16 = 2 ∨ 2 ^ b % 16 = 4 ∨ 2 ^ b % 16 = 8 ∨ 2 ^ b % 16 = 0 := by rcases lt_or_ge b 4 with hb4 | hb4 · have hbsmall : b = 1 ∨ b = 2 ∨ b = 3 := by omega rcases hbsmall with rfl | rfl | rfl · exact Or.inl (by norm_num) · exact Or.inr (Or.inl (by norm_num)) · exact Or.inr (Or.inr (Or.inl (by norm_num))) · exact Or.inr (Or.inr (Or.inr (two_pow_mod_sixteen_zero hb4))) have hpmodclass : p % 16 = 3 ∨ p % 16 = 5 ∨ p % 16 = 1 := by rcases hpclass with rfl | rfl | hpmod · exact Or.inl (by norm_num) · exact Or.inr (Or.inl (by norm_num)) · exact Or.inr (Or.inr hpmod) rcases hpmodclass with hpmod | hpmod | hpmod <;> rcases hbclass with hbmod | hbmod | hbmod | hbmod <;> simp [Nat.add_mod, hpmod, hamod, hbmod] at hmod lemma BF_dvd_CP {r n : ℕ} (hr : r < n) : BF r ∣ CP n := by by_cases h10 : r = 10 · subst r simp [BF, CP] · have hmem : r ∈ (Finset.range n).erase 10 := by simp [h10, hr] have hdiv : Nat.fermatNumber r ∣ ∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i := Finset.dvd_prod_of_mem Nat.fermatNumber hmem rcases hdiv with ⟨c, hc⟩ refine ⟨CD * c, ?_⟩ simp only [BF, if_neg h10, CP] rw [hc] ring lemma fermatNumber_dvd_pow_add_one {r u : ℕ} (hu : Odd u) : Nat.fermatNumber r ∣ 2 ^ (2 ^ r * u) + 1 := by have h := hu.nat_add_dvd_pow_add_pow (2 ^ (2 ^ r)) 1 simpa [Nat.fermatNumber, pow_mul] using h lemma BF_dvd_two_pow_sum {a b r u : ℕ} (hba : b ≤ a) (hdiff : a - b = 2 ^ r * u) (hu : Odd u) : BF r ∣ 2 ^ a + 2 ^ b := by have hF : Nat.fermatNumber r ∣ 2 ^ (a - b) + 1 := by rw [hdiff] exact fermatNumber_dvd_pow_add_one hu have hBF : BF r ∣ Nat.fermatNumber r := by by_cases h10 : r = 10 · subst r simp only [BF] exact ⟨CG, CD_mul_CG.symm⟩ · simp [BF, h10] rcases hBF.trans hF with ⟨c, hc⟩ refine ⟨2 ^ b * c, ?_⟩ have hab : a = (a - b) + b := by omega rw [hab, pow_add] calc 2 ^ (a - b) * 2 ^ b + 2 ^ b = 2 ^ b * (2 ^ (a - b) + 1) := by ring _ = 2 ^ b * (BF r * c) := by rw [hc] _ = BF r * (2 ^ b * c) := by ring lemma CA_not_prime_plus_two_positive_powers_ordered (j a b p : ℕ) (hb : 0 < b) (hba : b ≤ a) (hp : p.Prime) : CA j ≠ p + 2 ^ a + 2 ^ b := by intro heq rcases eq_or_lt_of_le hba with hEq | hLt · subst b apply CA_not_prime_plus_power j (a + 1) p hp calc CA j = p + 2 ^ a + 2 ^ a := heq _ = p + 2 ^ (a + 1) := by rw [pow_succ]; ring · have hp_pos : 0 < p := hp.pos have hpb_pos : 0 < 2 ^ b := by positivity have hpowA : 2 ^ a < CA j := by omega have hpowX : 2 ^ a < 2 ^ (2 ^ CL j) := lt_trans hpowA (CA_lt_power j) have haL : a < 2 ^ CL j := (Nat.pow_lt_pow_iff_right (by norm_num : 1 < 2)).mp hpowX have hdiff_ne : a - b ≠ 0 := by omega obtain ⟨r, u, hu, hdiff⟩ := Nat.exists_eq_two_pow_mul_odd hdiff_ne have hupos : 0 < u := hu.pos have huone : 1 ≤ u := by omega have hpowr_le : 2 ^ r ≤ a - b := by calc 2 ^ r = 2 ^ r * 1 := by simp _ ≤ 2 ^ r * u := Nat.mul_le_mul_left (2 ^ r) huone _ = a - b := hdiff.symm have hpowr_lt : 2 ^ r < 2 ^ CL j := lt_of_le_of_lt (le_trans hpowr_le (Nat.sub_le a b)) haL have hrL : r < CL j := (Nat.pow_lt_pow_iff_right (by norm_num : 1 < 2)).mp hpowr_lt have hBS : BF r ∣ 2 ^ a + 2 ^ b := BF_dvd_two_pow_sum (Nat.le_of_lt hLt) hdiff hu have hBA : BF r ∣ CA j := by rcases BF_dvd_CP hrL with ⟨c, hc⟩ refine ⟨CK * c, ?_⟩ simp only [CA] rw [hc] ring have hA0 : CA j ≡ 0 [MOD BF r] := Nat.modEq_zero_iff_dvd.mpr hBA have hS0 : 2 ^ a + 2 ^ b ≡ 0 [MOD BF r] := Nat.modEq_zero_iff_dvd.mpr hBS have hrepr : p + (2 ^ a + 2 ^ b) ≡ 0 [MOD BF r] := by calc p + (2 ^ a + 2 ^ b) = p + 2 ^ a + 2 ^ b := by ring _ = CA j := heq.symm _ ≡ 0 [MOD BF r] := hA0 have hpzero : p ≡ 0 [MOD BF r] := by apply Nat.ModEq.add_right_cancel' (2 ^ a + 2 ^ b) simpa using hrepr.trans hS0.symm have hdiv : BF r ∣ p := Nat.modEq_zero_iff_dvd.mp hpzero rcases (Nat.dvd_prime hp).mp hdiv with hbone | hbp · have hgt := BF_one_lt r omega · have hpclass : p = 3 ∨ p = 5 ∨ p % 16 = 1 := by simpa [hbp] using BF_residue_class r have hmod : (p + 2 ^ a + 2 ^ b) % 16 = 15 := by rw [← heq] exact CA_mod_sixteen j rcases two_power_residue_class hb hLt hpclass hmod with hcase | hcase · rcases hcase with ⟨rfl, rfl, rfl⟩ have hgt := CA_gt_fifteen j norm_num at heq omega · rcases hcase with ⟨rfl, rfl, rfl⟩ have hgt := CA_gt_fifteen j norm_num at heq omega lemma CA_not_prime_plus_two_positive_powers (j a b p : ℕ) (ha : 0 < a) (hb : 0 < b) (hp : p.Prime) : CA j ≠ p + 2 ^ a + 2 ^ b := by intro heq rcases le_total b a with hba | hab · exact CA_not_prime_plus_two_positive_powers_ordered j a b p hb hba hp heq · apply CA_not_prime_plus_two_positive_powers_ordered j b a p ha hab hp calc CA j = p + 2 ^ a + 2 ^ b := heq _ = p + 2 ^ b + 2 ^ a := by ring def CN (j : ℕ) : ℕ := CA j + 1 lemma CN_even (j : ℕ) : Even (CN j) := by have hmod := CA_mod_sixteen j have hdiv := Nat.div_add_mod (CA j) 16 refine ⟨8 * (CA j / 16) + 8, ?_⟩ simp only [CN] omega lemma multiset_card_le_three_cases {α : Type*} (s : Multiset α) (hs : s.card ≤ 3) : s = 0 ∨ (∃ a, s = {a}) ∨ (∃ a b, s = {a, b}) ∨ (∃ a b c, s = {a, b, c}) := by have hc : s.card = 0 ∨ s.card = 1 ∨ s.card = 2 ∨ s.card = 3 := by omega rcases hc with h0 | h1 | h2 | h3 · exact Or.inl (Multiset.card_eq_zero.mp h0) · exact Or.inr (Or.inl (Multiset.card_eq_one.mp h1)) · exact Or.inr (Or.inr (Or.inl (Multiset.card_eq_two.mp h2))) · exact Or.inr (Or.inr (Or.inr (Multiset.card_eq_three.mp h3))) lemma pow_two_mod_sixteen_cases (a : ℕ) : (a = 0 ∧ 2 ^ a % 16 = 1) ∨ (a = 1 ∧ 2 ^ a % 16 = 2) ∨ (a = 2 ∧ 2 ^ a % 16 = 4) ∨ (a = 3 ∧ 2 ^ a % 16 = 8) ∨ (4 ≤ a ∧ 2 ^ a % 16 = 0) := by rcases lt_or_ge a 4 with ha | ha · have hsmall : a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3 := by omega rcases hsmall with rfl | rfl | rfl | rfl <;> norm_num · exact Or.inr (Or.inr (Or.inr (Or.inr ⟨ha, two_pow_mod_sixteen_zero ha⟩))) lemma one_power_not_mod_sixteen_fourteen (a : ℕ) : 2 ^ a % 16 ≠ 14 := by intro hmod rcases pow_two_mod_sixteen_cases a with ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨ha_ge, ha⟩ · norm_num at hmod · norm_num at hmod · norm_num at hmod · norm_num at hmod · omega lemma two_powers_not_mod_sixteen_fourteen (a b : ℕ) : (2 ^ a + 2 ^ b) % 16 ≠ 14 := by intro hmod rcases pow_two_mod_sixteen_cases a with ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨ha_ge, ha⟩ <;> rcases pow_two_mod_sixteen_cases b with ⟨rfl, hb⟩ | ⟨rfl, hb⟩ | ⟨rfl, hb⟩ | ⟨rfl, hb⟩ | ⟨hb_ge, hb⟩ <;> simp [Nat.add_mod, ha, hb] at hmod lemma three_powers_mod_sixteen_fourteen {a b c : ℕ} (hmod : (2 ^ a + 2 ^ b + 2 ^ c) % 16 = 14) : 2 ^ a + 2 ^ b + 2 ^ c = 14 := by rcases pow_two_mod_sixteen_cases a with ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨ha_ge, ha⟩ <;> rcases pow_two_mod_sixteen_cases b with ⟨rfl, hb⟩ | ⟨rfl, hb⟩ | ⟨rfl, hb⟩ | ⟨rfl, hb⟩ | ⟨hb_ge, hb⟩ <;> rcases pow_two_mod_sixteen_cases c with ⟨rfl, hc⟩ | ⟨rfl, hc⟩ | ⟨rfl, hc⟩ | ⟨rfl, hc⟩ | ⟨hc_ge, hc⟩ <;> simp [Nat.add_mod, ha, hb, hc] at hmod ⊢ lemma pow_two_eq_two_mul_pre {a : ℕ} (ha : 0 < a) : 2 ^ a = 2 * 2 ^ (a - 1) := by have hsplit : a = 1 + (a - 1) := by omega rw [hsplit, pow_add] norm_num lemma mod_two_one_one_pow {c : ℕ} (hc : 0 < c) : (1 + 1 + 2 ^ c) % 2 = 0 := by rw [pow_two_eq_two_mul_pre hc] have h : 1 + 1 + 2 * 2 ^ (c - 1) = 2 * (1 + 2 ^ (c - 1)) := by ring rw [h] simp lemma mod_two_one_pow_one {b : ℕ} (hb : 0 < b) : (1 + 2 ^ b + 1) % 2 = 0 := by rw [pow_two_eq_two_mul_pre hb] have h : 1 + 2 * 2 ^ (b - 1) + 1 = 2 * (2 ^ (b - 1) + 1) := by ring rw [h] simp lemma mod_two_pow_one_one {a : ℕ} (ha : 0 < a) : (2 ^ a + 1 + 1) % 2 = 0 := by rw [pow_two_eq_two_mul_pre ha] have h : 2 * 2 ^ (a - 1) + 1 + 1 = 2 * (2 ^ (a - 1) + 1) := by ring rw [h] simp lemma mod_two_three_positive_pows {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (2 ^ a + 2 ^ b + 2 ^ c) % 2 = 0 := by rw [pow_two_eq_two_mul_pre ha, pow_two_eq_two_mul_pre hb, pow_two_eq_two_mul_pre hc] have h : 2 * 2 ^ (a - 1) + 2 * 2 ^ (b - 1) + 2 * 2 ^ (c - 1) = 2 * (2 ^ (a - 1) + 2 ^ (b - 1) + 2 ^ (c - 1)) := by ring rw [h] simp lemma CN_mod_two (j : ℕ) : CN j % 2 = 0 := by rcases CN_even j with ⟨k, hk⟩ rw [hk] omega lemma CN_mod_sixteen (j : ℕ) : CN j % 16 = 0 := by simp [CN, Nat.add_mod, CA_mod_sixteen] lemma two_pow_mod_two_zero {a : ℕ} (ha : 0 < a) : 2 ^ a % 2 = 0 := by have hsplit : a = 1 + (a - 1) := by omega rw [hsplit, pow_add] norm_num lemma prime_mod_two_one {p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2) : p % 2 = 1 := by have hlt : p % 2 < 2 := Nat.mod_lt _ (by norm_num) by_contra hne have hz : p % 2 = 0 := by omega have hdvd : 2 ∣ p := Nat.dvd_iff_mod_eq_zero.mpr hz have heq : 2 = p := (Nat.prime_dvd_prime_iff_eq (by norm_num) hp).mp hdvd exact hp2 heq.symm lemma CN_odd_prime_even_sum_impossible (j p s : ℕ) (hpmod : p % 2 = 1) (hsmod : s % 2 = 0) (heq : CN j = p + s) : False := by have hmod : (p + s) % 2 = 0 := by rw [← heq] exact CN_mod_two j simp [Nat.add_mod, hpmod, hsmod] at hmod lemma mapped_pow_sum_singleton (a : ℕ) : (({a} : Multiset ℕ).map (fun x => 2 ^ x)).sum = 2 ^ a := by simp lemma mapped_pow_sum_pair (a b : ℕ) : (({a, b} : Multiset ℕ).map (fun x => 2 ^ x)).sum = 2 ^ a + 2 ^ b := by simp lemma mapped_pow_sum_triple (a b c : ℕ) : (({a, b, c} : Multiset ℕ).map (fun x => 2 ^ x)).sum = 2 ^ a + 2 ^ b + 2 ^ c := by simp ring abbrev SumPrimeThreePows : Set ℕ := Erdos10.sumPrimeAndTwoPows 3 lemma CN_not_sumPrimeThreePows (j : ℕ) : CN j ∉ SumPrimeThreePows := by intro hmem rcases hmem with ⟨p, pows, hp, hcard, heq⟩ have heq' : CN j = p + (pows.map (2 ^ ·)).sum := heq.symm rcases multiset_card_le_three_cases pows hcard with hzero | ⟨a, hone⟩ | ⟨a, b, htwo⟩ | ⟨a, b, c, hthree⟩ · subst pows simp only [Multiset.map_zero, Multiset.sum_zero, add_zero] at heq' by_cases hp2 : p = 2 · rw [hp2] at heq' have hgt := CA_gt_fifteen j simp [CN] at heq' omega · exact CN_odd_prime_even_sum_impossible j p 0 (prime_mod_two_one hp hp2) (by norm_num) (by simpa using heq') · subst pows rw [mapped_pow_sum_singleton] at heq' by_cases hp2 : p = 2 · rw [hp2] at heq' have hreprmod : (2 + 2 ^ a) % 16 = 0 := by rw [← heq'] exact CN_mod_sixteen j have hsumMod : 2 ^ a % 16 = 14 := by rw [Nat.add_mod] at hreprmod have hlt := Nat.mod_lt (2 ^ a) (by norm_num : 0 < 16) omega exact one_power_not_mod_sixteen_fourteen a hsumMod · have hpmod := prime_mod_two_one hp hp2 by_cases ha0 : a = 0 · subst a have hA : CA j = p := by simp [CN] at heq' omega have hpA : (CA j).Prime := by simpa [hA] using hp exact CA_not_prime j hpA · have ha : 0 < a := Nat.pos_of_ne_zero ha0 exact CN_odd_prime_even_sum_impossible j p (2 ^ a) hpmod (two_pow_mod_two_zero ha) heq' · subst pows rw [mapped_pow_sum_pair] at heq' by_cases hp2 : p = 2 · rw [hp2] at heq' have hform : CN j = 2 + 2 ^ a + 2 ^ b := by omega have hreprmod : (2 + (2 ^ a + 2 ^ b)) % 16 = 0 := by have hform' : CN j = 2 + (2 ^ a + 2 ^ b) := by omega exact (congrArg (fun n : ℕ => n % 16) hform'.symm).trans (CN_mod_sixteen j) have hsumMod : (2 ^ a + 2 ^ b) % 16 = 14 := by rw [Nat.add_mod] at hreprmod have hlt := Nat.mod_lt (2 ^ a + 2 ^ b) (by norm_num : 0 < 16) omega exact two_powers_not_mod_sixteen_fourteen a b hsumMod · have hpmod := prime_mod_two_one hp hp2 by_cases ha0 : a = 0 · subst a by_cases hb0 : b = 0 · subst b have hform : CN j = p + 2 := by omega exact CN_odd_prime_even_sum_impossible j p 2 hpmod (by norm_num) hform · have hb : 0 < b := Nat.pos_of_ne_zero hb0 have hA : CA j = p + 2 ^ b := by simp [CN] at heq' omega exact CA_not_prime_plus_power j b p hp hA · have ha : 0 < a := Nat.pos_of_ne_zero ha0 by_cases hb0 : b = 0 · subst b have hA : CA j = p + 2 ^ a := by simp [CN] at heq' omega exact CA_not_prime_plus_power j a p hp hA · have hb : 0 < b := Nat.pos_of_ne_zero hb0 have hsmod : (2 ^ a + 2 ^ b) % 2 = 0 := by simp [Nat.add_mod, two_pow_mod_two_zero ha, two_pow_mod_two_zero hb] have hform : CN j = p + (2 ^ a + 2 ^ b) := by omega exact CN_odd_prime_even_sum_impossible j p (2 ^ a + 2 ^ b) hpmod hsmod hform · subst pows rw [mapped_pow_sum_triple] at heq' by_cases hp2 : p = 2 · rw [hp2] at heq' have hform : CN j = 2 + (2 ^ a + 2 ^ b + 2 ^ c) := by omega have hreprmod : (2 + (2 ^ a + 2 ^ b + 2 ^ c)) % 16 = 0 := (congrArg (fun n : ℕ => n % 16) hform.symm).trans (CN_mod_sixteen j) have hsumMod : (2 ^ a + 2 ^ b + 2 ^ c) % 16 = 14 := by rw [Nat.add_mod] at hreprmod have hlt := Nat.mod_lt (2 ^ a + 2 ^ b + 2 ^ c) (by norm_num : 0 < 16) omega have hsum := three_powers_mod_sixteen_fourteen hsumMod have hgt := CA_gt_fifteen j simp [CN] at heq' omega · have hpmod := prime_mod_two_one hp hp2 by_cases ha0 : a = 0 · subst a by_cases hb0 : b = 0 · subst b by_cases hc0 : c = 0 · subst c have hA : CA j = p + 2 ^ 1 := by simp [CN] at heq' omega exact CA_not_prime_plus_power j 1 p hp hA · have hc : 0 < c := Nat.pos_of_ne_zero hc0 have hsmod : (1 + 1 + 2 ^ c) % 2 = 0 := mod_two_one_one_pow hc have hform : CN j = p + (1 + 1 + 2 ^ c) := by omega exact CN_odd_prime_even_sum_impossible j p (1 + 1 + 2 ^ c) hpmod hsmod hform · have hb : 0 < b := Nat.pos_of_ne_zero hb0 by_cases hc0 : c = 0 · subst c have hsmod : (1 + 2 ^ b + 1) % 2 = 0 := mod_two_one_pow_one hb have hform : CN j = p + (1 + 2 ^ b + 1) := by omega exact CN_odd_prime_even_sum_impossible j p (1 + 2 ^ b + 1) hpmod hsmod hform · have hc : 0 < c := Nat.pos_of_ne_zero hc0 have hA : CA j = p + 2 ^ b + 2 ^ c := by simp [CN] at heq' omega exact CA_not_prime_plus_two_positive_powers j b c p hb hc hp hA · have ha : 0 < a := Nat.pos_of_ne_zero ha0 by_cases hb0 : b = 0 · subst b by_cases hc0 : c = 0 · subst c have hsmod : (2 ^ a + 1 + 1) % 2 = 0 := mod_two_pow_one_one ha have hform : CN j = p + (2 ^ a + 1 + 1) := by omega exact CN_odd_prime_even_sum_impossible j p (2 ^ a + 1 + 1) hpmod hsmod hform · have hc : 0 < c := Nat.pos_of_ne_zero hc0 have hA : CA j = p + 2 ^ a + 2 ^ c := by simp [CN] at heq' omega exact CA_not_prime_plus_two_positive_powers j a c p ha hc hp hA · have hb : 0 < b := Nat.pos_of_ne_zero hb0 by_cases hc0 : c = 0 · subst c have hA : CA j = p + 2 ^ a + 2 ^ b := by simp [CN] at heq' omega exact CA_not_prime_plus_two_positive_powers j a b p ha hb hp hA · have hc : 0 < c := Nat.pos_of_ne_zero hc0 have hsmod : (2 ^ a + 2 ^ b + 2 ^ c) % 2 = 0 := mod_two_three_positive_pows ha hb hc have hform : CN j = p + (2 ^ a + 2 ^ b + 2 ^ c) := by omega exact CN_odd_prime_even_sum_impossible j p (2 ^ a + 2 ^ b + 2 ^ c) hpmod hsmod hform lemma CL_strictMono : StrictMono CL := by intro a b hab simp only [CL] omega lemma outer_power_strictMono : StrictMono (fun j : ℕ => 2 ^ (2 ^ CL j)) := by intro a b hab apply (Nat.pow_lt_pow_iff_right (by norm_num : 1 < 2)).mpr apply (Nat.pow_lt_pow_iff_right (by norm_num : 1 < 2)).mpr exact CL_strictMono hab lemma CP_CL_strictMono : StrictMono (fun j : ℕ => CP (CL j)) := by intro a b hab have hX := outer_power_strictMono hab have ha := CP_mul_CG_add_one (CL_gt_ten a) have hb := CP_mul_CG_add_one (CL_gt_ten b) have hmulAdd : CP (CL a) * CG + 1 < CP (CL b) * CG + 1 := by calc CP (CL a) * CG + 1 = 2 ^ (2 ^ CL a) := ha _ < 2 ^ (2 ^ CL b) := hX _ = CP (CL b) * CG + 1 := hb.symm have hmul : CP (CL a) * CG < CP (CL b) * CG := by omega have hG : 0 < CG := by norm_num [CG] exact (Nat.mul_lt_mul_right hG).mp hmul lemma CA_strictMono : StrictMono CA := by intro a b hab have hp := CP_CL_strictMono hab have hk : 0 < CK := by norm_num [CK] exact Nat.mul_lt_mul_of_pos_left hp hk lemma CN_strictMono : StrictMono CN := by intro a b hab have hA := CA_strictMono hab simp only [CN] omega lemma CN_range_subset : Set.range CN ⊆ {n : ℕ | Even n} \ SumPrimeThreePows := by rintro n ⟨j, rfl⟩ exact ⟨CN_even j, CN_not_sumPrimeThreePows j⟩ lemma local_grechuk_target : Set.Infinite ({n : ℕ | Even n} \ SumPrimeThreePows) := by exact (Set.infinite_range_of_injective CN_strictMono.injective).mono CN_range_subset theorem target : fcTypeOfName% "Erdos10.erdos_10.variants.grechuk" := by exact local_grechuk_target