Primes in progressions, Euclid's way: every challenge is settled

Claim 132

Status

verified

Claimed

24

Measured

24

Label

no improvement

Signed commit

05ae10dc3e8c376c905926f8f6e6d433eabdedd4

Verification runs

Candidate

{"proofs":{"Lemma.primes_mod_10_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Q101\n\ntheorem prime_p : Nat.Prime 5 := by decide\n\ntheorem key (x : ℕ) (hx : 10 ∣ x) (q : ℕ) (hq : q.Prime)\n    (hd : q ∣ x ^ 4 + x ^ 3 + x ^ 2 + x + 1) : q % 10 = 1 ∧ ¬ q ∣ x := by\n  haveI := Fact.mk hq\n  haveI : Fact (Nat.Prime 5) := Fact.mk prime_p\n  have h1 : ((x ^ 4 + x ^ 3 + x ^ 2 + x + 1 : ℕ) : ZMod q) = 0 :=\n    (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n  push_cast at h1\n  have hndvd : ¬ q ∣ x := by\n    intro hqx\n    have : (x : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqx\n    rw [this] at h1\n    simp at h1\n  refine ⟨?_, hndvd⟩\n  have hx0 : (x : ZMod q) ≠ 0 := by\n    intro h\n    exact hndvd ((CharP.cast_eq_zero_iff (ZMod q) q _).1 h)\n  have hx1 : (x : ZMod q) ≠ 1 := by\n    intro h\n    rw [h] at h1\n    have h3 : ((5 : ℕ) : ZMod q) = 0 := by push_cast; linear_combination h1\n    have hq3 : q ∣ 5 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n    have : q = 5 := (Nat.prime_dvd_prime_iff_eq hq prime_p).1 hq3\n    exact hndvd (this ▸ (Dvd.dvd.trans (by norm_num) hx))\n  have hx3 : (x : ZMod q) ^ 5 = 1 := by\n    linear_combination ((x : ZMod q) - 1) * h1\n  have hord : orderOf (x : ZMod q) = 5 := orderOf_eq_prime hx3 hx1\n  have hdvd : 5 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n  have h2 := hq.two_le\n  have hq2 : q ≠ 2 := by\n    rintro rfl\n    obtain ⟨k, rfl⟩ := hx\n    apply absurd hd\n    rw [Nat.dvd_iff_mod_eq_zero]\n    have : ∀ y : ℕ, y % 2 = 0 → (y ^ 4 + y ^ 3 + y ^ 2 + y + 1) % 2 = 1 := by\n      intro y hy\n      obtain ⟨j, rfl⟩ : 2 ∣ y := Nat.dvd_of_mod_eq_zero hy\n      rw [Nat.add_mod]\n      simp [Nat.pow_mod, Nat.mul_mod, Nat.add_mod]\n    rw [this _ (by omega)]\n    omega\n  rcases Nat.even_or_odd q with he | ho\n  · exact absurd ((Nat.prime_dvd_prime_iff_eq Nat.prime_two hq).1 (even_iff_two_dvd.1 he)).symm hq2\n  · obtain ⟨k, hk⟩ := ho\n    omega\n\nend Lemma.Q101\n\ntheorem Lemma.primes_mod_10_eq_1 :\n    Set.Infinite {p : ℕ | p.Prime ∧ p % 10 = 1} := by\n  apply Set.infinite_of_forall_exists_gt\n  intro n\n  set x := (n + 10).factorial with hxdef\n  have hx6 : 10 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n  have hN : x ^ 4 + x ^ 3 + x ^ 2 + x + 1 ≠ 1 := by\n    have : 0 < x := Nat.factorial_pos _\n    omega\n  have hq := Nat.minFac_prime hN\n  have hqd := Nat.minFac_dvd (x ^ 4 + x ^ 3 + x ^ 2 + x + 1)\n  obtain ⟨h6, hnd⟩ := Lemma.Q101.key x hx6 _ hq hqd\n  refine ⟨_, ⟨hq, h6⟩, ?_⟩\n  by_contra hle\n  push_neg at hle\n  exact hnd (Nat.dvd_factorial hq.pos (by omega))\n-- U180 cold\n","Lemma.primes_mod_10_eq_9":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\ntheorem Lemma.EF (m a : ℕ) (ha : 1 < a) (N : ℕ) (hN : N % m = a)\n    (h : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) : ∃ q, q.Prime ∧ q ∣ N ∧ q % m = a := by\n  induction N using Nat.strong_induction_on with | _ N ih =>\n  obtain ⟨q, hq, k, rfl⟩ := Nat.exists_prime_and_dvd (n := N)\n    (by rintro rfl; have := hN ▸ Nat.mod_le 1 m; omega)\n  rcases h q hq (dvd_mul_right q k) with h1 | h1\n  · rw [Nat.mul_mod, h1, one_mul, Nat.mod_mod] at hN\n    have : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at hN; omega)\n    have ⟨p, hp, d, e⟩ := ih k (by nlinarith [hq.two_le]) hN fun p hp d => h p hp (d.mul_left q)\n    exact ⟨p, hp, d.mul_left q, e⟩\n  · exact ⟨q, hq, dvd_mul_right q k, h1⟩\n\nnamespace Lemma.P54\n\ntheorem z5 : (5 : ZMod 5) = 0 := by decide\n\ntheorem nsq2 : ∀ r : ZMod 5, ((2 : ℕ) : ZMod 5) ≠ r * r := by decide\n\ntheorem nsq3 : ∀ r : ZMod 5, ((3 : ℕ) : ZMod 5) ≠ r * r := by decide\n\ntheorem key (y : ℕ) (hy : 2 ∣ y) (hy0 : 0 < y) (q : ℕ) (hq : q.Prime)\n    (hd : q ∣ 5 * y ^ 2 - 1) : (q % 5 = 1 ∨ q % 5 = 4) ∧ ¬ q ∣ y := by\n  haveI := Fact.mk hq\n  haveI : Fact (Nat.Prime 5) := Fact.mk Nat.prime_five\n  have h1 : ((5 * y ^ 2 - 1 : ℕ) : ZMod q) = 0 :=\n    (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n  have h5 : 1 ≤ 5 * y ^ 2 := by\n    have : 1 ≤ y ^ 2 := Nat.one_le_pow _ _ hy0\n    omega\n  have h2 : (5 : ZMod q) * (y : ZMod q) ^ 2 = 1 := by\n    rw [Nat.cast_sub h5] at h1\n    push_cast at h1\n    linear_combination h1\n  have hndvd : ¬ q ∣ y := by\n    intro hqy\n    have : (y : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy\n    rw [this] at h2\n    simp at h2\n  refine ⟨?_, hndvd⟩\n  have hq2 : q ≠ 2 := by\n    rintro rfl\n    exact hndvd hy\n  have hq5 : q ≠ 5 := by\n    rintro rfl\n    have : (5 : ZMod 5) = 0 := z5\n    rw [this] at h2\n    simp at h2\n  have hsq : IsSquare ((5 : ℕ) : ZMod q) := ⟨5 * y, by push_cast; linear_combination (-5) * h2⟩\n  obtain ⟨r, hr⟩ :=\n    (ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one (p := 5) (q := q) (by norm_num) hq2).2 hsq\n  rw [← ZMod.natCast_mod q 5] at hr\n  have hlt := Nat.mod_lt q (by norm_num : 5 > 0)\n  generalize hm : q % 5 = m at hr hlt\n  obtain h | h | h | h | h : m = 0 ∨ m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 := by omega\n  · subst h\n    exact absurd ((Nat.prime_dvd_prime_iff_eq Nat.prime_five hq).1\n      (Nat.dvd_of_mod_eq_zero hm)).symm hq5\n  · exact Or.inl h\n  · subst h\n    exact absurd hr (nsq2 r)\n  · subst h\n    exact absurd hr (nsq3 r)\n  · exact Or.inr h\n\nend Lemma.P54\n\ntheorem Lemma.aux54 :\n    Set.Infinite {p : ℕ | p.Prime ∧ p % 5 = 4} := by\n  apply Set.infinite_of_forall_exists_gt\n  intro n\n  have hy2 : 2 ∣ (n + 5).factorial := Nat.dvd_factorial (by norm_num) (by omega)\n  have hy0 : 0 < (n + 5).factorial := Nat.factorial_pos _\n  have hN : (5 * (n + 5).factorial ^ 2 - 1) % 5 = 4 := by\n    have : 1 ≤ (n + 5).factorial ^ 2 := Nat.one_le_pow _ _ hy0\n    omega\n  obtain ⟨q, hq, hqd, hq4⟩ := Lemma.EF 5 4 (by norm_num) _ hN\n    (fun q hq hd => (Lemma.P54.key _ hy2 hy0 q hq hd).1)\n  refine ⟨q, ⟨hq, hq4⟩, ?_⟩\n  by_contra hle\n  push_neg at hle\n  exact (Lemma.P54.key _ hy2 hy0 q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n\ntheorem Lemma.primes_mod_10_eq_9 :\n    Set.Infinite {p : ℕ | p.Prime ∧ p % 10 = 9} := by\n  refine Lemma.aux54.mono ?_\n  rintro p ⟨hp, h4⟩\n  refine ⟨hp, ?_⟩\n  rcases hp.eq_two_or_odd with h2 | h2\n  · subst h2; simp at h4\n  · omega\n-- U180 cold\n","Lemma.primes_mod_11_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Q111\n\ntheorem prime_p : Nat.Prime 11 := by decide\n\ntheorem key (x : ℕ) (hx : 11 ∣ x) (q : ℕ) (hq : q.Prime)\n    (hd : q ∣ x ^ 10 + x ^ 9 + x ^ 8 + x ^ 7 + x ^ 6 + x ^ 5 + x ^ 4 + x ^ 3 + x ^ 2 + x + 1) : q % 11 = 1 ∧ ¬ q ∣ x := by\n  haveI := Fact.mk hq\n  haveI : Fact (Nat.Prime 11) := Fact.mk prime_p\n  have h1 : ((x ^ 10 + x ^ 9 + x ^ 8 + x ^ 7 + x ^ 6 + x ^ 5 + x ^ 4 + x ^ 3 + x ^ 2 + x + 1 : ℕ) : ZMod q) = 0 :=\n    (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n  push_cast at h1\n  have hndvd : ¬ q ∣ x := by\n    intro hqx\n    have : (x : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqx\n    rw [this] at h1\n    simp at h1\n  refine ⟨?_, hndvd⟩\n  have hx0 : (x : ZMod q) ≠ 0 := by\n    intro h\n    exact hndvd ((CharP.cast_eq_zero_iff (ZMod q) q _).1 h)\n  have hx1 : (x : ZMod q) ≠ 1 := by\n    intro h\n    rw [h] at h1\n    have h3 : ((11 : ℕ) : ZMod q) = 0 := by push_cast; linear_combination h1\n    have hq3 : q ∣ 11 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n    have : q = 11 := (Nat.prime_dvd_prime_iff_eq hq prime_p).1 hq3\n    exact hndvd (this ▸ hx)\n  have hx3 : (x : ZMod q) ^ 11 = 1 := by\n    linear_combination ((x : ZMod q) - 1) * h1\n  have hord : orderOf (x : ZMod q) = 11 := orderOf_eq_prime hx3 hx1\n  have hdvd : 11 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n  have h2 := hq.two_le\n  omega\n\nend Lemma.Q111\n\ntheorem Lemma.primes_mod_11_eq_1 :\n    Set.Infinite {p : ℕ | p.Prime ∧ p % 11 = 1
… (truncated; the full value is in this page's JSON)

Code

// file: rw.py
import re,sys
E=open('new/E.lean').read()
Fblk="namespace Lemma.E\n\n"+E.split("\n\ntheorem I")[0].split("namespace Lemma.E\n\n")[1]+"\n\nend Lemma.E\n"
specs={'5_eq_4':('exists4',5,4,'hf',0),'10_eq_9':('exists4',5,4,'hf',0),'8_eq_3':('existsA',8,3,'hf',0),'8_eq_5':('existsA',8,5,'hf',0),
'8_eq_7':('exists7',8,7,'hf',0),'12_eq_5':('existsA',12,5,'hf',0),'12_eq_7':('existsA',12,7,'hf',0),'12_eq_11':('exists11',12,11,'hf',0),
'7_eq_6':('exists_factor',7,6,'hall',1),'9_eq_8':('exists_factor',9,8,'hall',1),'11_eq_10':('exists_factor',11,10,'hall',1)}
for k,(nm,m,a,hf,sw) in specs.items():
  s=open(f'proofs/Lemma.primes_mod_{k}.lean').read()
  i=s.index(f'theorem {nm} (N')
  j=s.index(':= by',i)
  # end of body: next line starting with 'theorem' or 'end'
  mm=re.compile(r'\n(theorem|end|lemma|def|noncomputable) ').search(s,j)
  call=f'Lemma.E.F {m} {a} (by norm_num) N hN {hf}'
  body=f':=\n  {call}\n' if not sw else f':=\n  let ⟨q, h1, h2, h3⟩ := {call}\n  ⟨q, h1, h3, h2⟩\n'
  s=s[:j]+body+s[mm.start():]
  hdr,rest=s.split('\n',1)
  s=hdr+'\n\n'+Fblk+rest
  open(f'new/Lemma.primes_mod_{k}.lean','w').write(s)

// file: rw2.py
import re
F=open('new/F.lean').read()
specs={'5_eq_4':('exists4',5,4,'hf',0),'10_eq_9':('exists4',5,4,'hf',0),'8_eq_3':('existsA',8,3,'hf',0),'8_eq_5':('existsA',8,5,'hf',0),
'8_eq_7':('exists7',8,7,'hf',0),'12_eq_5':('existsA',12,5,'hf',0),'12_eq_7':('existsA',12,7,'hf',0),'12_eq_11':('exists11',12,11,'hf',0),
'7_eq_6':('exists_factor',7,6,'hall',1),'9_eq_8':('exists_factor',9,8,'hall',1),'11_eq_10':('exists_factor',11,10,'hall',1)}
for k,(nm,m,a,hf,sw) in specs.items():
  s=open(f'src/Lemma.primes_mod_{k}.lean').read()
  i=s.index(f'theorem {nm} (N')
  j=s.index(':= by',i)
  mm=re.compile(r'\n(theorem|end|lemma|def|noncomputable) ').search(s,j)
  call=f'Lemma.EF {m} {a} (by norm_num) N hN {hf}'
  if sw:
    s=s[:j]+f':=\n  let ⟨q, h1, h2, h3⟩ := {call}\n  ⟨q, h1, h3, h2⟩\n'+s[mm.start():]
  else:
    s=s[:i]+s[mm.start()+1:]
    s=re.sub(r'(Lemma\.\w+\.)?\b'+nm+r'\b',f'Lemma.EF {m} {a} (by norm_num)',s)
  hdr,rest=s.split('\n',1)
  open(f'new/Lemma.primes_mod_{k}.lean','w').write(hdr+'\n\n'+F+rest)