{"claim":{"assessments":[],"bundle":{"code":"","commit":"1036d0696eac4c7caab9aac7c8e33fcfde1cb7e3","config":null,"environment":"lemma/0.7.9 agent","logs":"","seeds":[]},"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","Lemma.primes_mod_10_eq_9":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\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\ntheorem exists4 (N : ℕ) (hN : N % 5 = 4)\n (hf : ∀ q, q.Prime → q ∣ N → q % 5 = 1 ∨ q % 5 = 4) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 5 = 4 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 5 = 4 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, 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.P54.exists4 _ 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","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} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 22).factorial with hxdef\n have hx6 : 11 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hN : x ^ 10 + x ^ 9 + x ^ 8 + x ^ 7 + x ^ 6 + x ^ 5 + 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 ^ 10 + x ^ 9 + x ^ 8 + x ^ 7 + x ^ 6 + x ^ 5 + x ^ 4 + x ^ 3 + x ^ 2 + x + 1)\n obtain ⟨h6, hnd⟩ := Lemma.Q111.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","Lemma.primes_mod_11_eq_10":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.RC\n\nopen Polynomial\n\n/-- Generic Frobenius step: if every root `r` of `X^2 - t X + 1` in a field extension of\n`ZMod q` has order `m`, then `m ∣ q - 1` or `m ∣ q + 1`. -/\ntheorem frob (q : ℕ) (hq : q.Prime) (t : ZMod q) (m : ℕ)\n (hord : ∀ (K : Type) [Field K] [Algebra (ZMod q) K] [CharP K q] (r : K),\n r ^ 2 - algebraMap (ZMod q) K t * r + 1 = 0 → orderOf r = m) :\n m ∣ q - 1 ∨ m ∣ q + 1 := by\n haveI := Fact.mk hq\n set p : (ZMod q)[X] := X ^ 2 - C t * X + 1 with hpdef\n have hp : p.natDegree = 2 := by rw [hpdef]; compute_degree!\n have hpu : ¬ IsUnit p := by\n intro h\n have := Polynomial.natDegree_eq_zero_of_isUnit h\n omega\n have hp0 : p ≠ 0 := by\n intro h\n rw [h] at hp\n simp at hp\n obtain ⟨g, hg, hgp⟩ := WfDvdMonoid.exists_irreducible_factor hpu hp0\n haveI := Fact.mk hg\n let K := AdjoinRoot g\n let r : K := AdjoinRoot.root g\n have hr0 : aeval r p = 0 := by\n obtain ⟨c, hc⟩ := hgp\n rw [hc, map_mul, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self, zero_mul]\n set T : K := algebraMap (ZMod q) K t with hTdef\n have hr : r ^ 2 - T * r + 1 = 0 := by\n rw [hpdef] at hr0\n simpa [hTdef] using hr0\n haveI : CharP K q := charP_of_injective_algebraMap (algebraMap (ZMod q) K).injective q\n have hord' : orderOf r = m := hord K r hr\n have hTq : T ^ q = T := by rw [hTdef, ← map_pow, ZMod.pow_card]\n have hrne : r ≠ 0 := by\n intro h0\n rw [h0] at hr\n simp at hr\n have hrq : (r ^ q) ^ 2 - T * r ^ q + 1 = 0 := by\n have : (r ^ 2 - T * r + 1) ^ q = 0 := by rw [hr, zero_pow hq.ne_zero]\n rw [add_pow_char, sub_pow_char, mul_pow, hTq, one_pow] at this\n rw [← this]\n ring\n have hprod : (r ^ q - r) * (r ^ q - (T - r)) = 0 := by linear_combination hrq - hr\n have hq2 := hq.two_le\n rw [← hord']\n rcases mul_eq_zero.1 hprod with h | h\n · left\n apply orderOf_dvd_of_pow_eq_one\n have e : r ^ q = r ^ (q - 1) * r := by\n rw [← pow_succ]; congr 1; omega\n have : (r ^ (q - 1) - 1) * r = 0 := by linear_combination e.symm.trans (sub_eq_zero.1 h)\n rcases mul_eq_zero.1 this with h2 | h2\n · exact sub_eq_zero.1 h2\n · exact absurd h2 hrne\n · right\n apply orderOf_dvd_of_pow_eq_one\n rw [pow_succ, sub_eq_zero.1 h]\n linear_combination -hr\n\n/-- Generic Euclid step: if every prime factor of `N` is `1` or `a` mod `m`, and `N ≡ a`,\nthen some prime factor is `a` mod `m`. -/\ntheorem exists_factor (m a : ℕ) (h1 : 1 % m ≠ a) (ha0 : a ≠ 0) (N : ℕ) (hN : N % m = a)\n (hall : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) :\n ∃ q, q.Prime ∧ q % m = a ∧ q ∣ N := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by rintro rfl; exact h1 hN\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n set q := N.minFac with hqdef\n rcases hall q hq hqd with hq1 | hqa\n · obtain ⟨k, hk⟩ := hqd\n have hmod := Nat.mul_mod q k m\n rw [hq1, ← hk, hN, one_mul, Nat.mod_mod] at hmod\n have hk0 : 0 < k := by\n apply Nat.pos_of_ne_zero\n rintro rfl\n rw [mul_zero] at hk\n rw [hk, Nat.zero_mod] at hN\n exact ha0 hN.symm\n have hklt : k < N := by\n rw [hk]\n calc k = 1 * k := (one_mul k).symm\n _ < q * k := Nat.mul_lt_mul_of_pos_right hq.one_lt hk0\n have hall' : ∀ r, r.Prime → r ∣ k → r % m = 1 ∨ r % m = a := fun r hr hrk =>\n hall r hr (hrk.trans ⟨q, by rw [hk, mul_comm]⟩)\n obtain ⟨r, hr, hra, hrd⟩ := ih k hklt hmod.symm hall'\n exact ⟨r, hr, hra, hrd.trans ⟨q, by rw [hk, mul_comm]⟩⟩\n · exact ⟨q, hq, hqa, hqd⟩\n\nend Lemma.RC\n\nnamespace Lemma.P1110\n\ntheorem prime11 : Nat.Prime 11 := by decide\n\ntheorem key (q : ℕ) (hq : q.Prime) (hq11 : q ≠ 11) (t : ZMod q)\n (ht : t ^ 5 + t ^ 4 - 4 * t ^ 3 - 3 * t ^ 2 + 3 * t + 1 = 0) :\n q % 11 = 1 ∨ q % 11 = 10 := by\n haveI : Fact (Nat.Prime 11) := Fact.mk prime11\n have h := Lemma.RC.frob q hq t 11 (by\n intro K _ _ _ r hr\n set T : K := algebraMap (ZMod q) K t with hTdef\n have hT : T ^ 5 + T ^ 4 - 4 * T ^ 3 - 3 * T ^ 2 + 3 * T + 1 = 0 := by\n have := congrArg (algebraMap (ZMod q) K) ht\n simpa [hTdef, map_ofNat] using this\n have hr11 : r ^ 11 = 1 := by\n linear_combination (r - 1) * (r ^ 5 * hT\n + (1 + r + r * T + r ^ 2 * T + r ^ 2 * T ^ 2 - r ^ 3 * T + r ^ 3 * T ^ 2 + r ^ 3 * T ^ 3\n + r ^ 4 - r ^ 4 * T - 2 * r ^ 4 * T ^ 2 + r ^ 4 * T ^ 3 + r ^ 4 * T ^ 4\n - r ^ 5 * T + r ^ 5 * T ^ 2 + r ^ 5 * T ^ 3 + r ^ 6 * T + r ^ 6 * T ^ 2\n + r ^ 7 + r ^ 7 * T + r ^ 8) * hr)\n have hr1 : r ≠ 1 := by\n intro h1\n rw [h1] at hr\n have hT2 : T = 2 := by linear_combination -hr\n rw [hT2] at hT\n have h11 : ((11 : ℕ) : K) = 0 := by push_cast; linear_combination hT\n exact hq11 ((Nat.prime_dvd_prime_iff_eq hq prime11).1 ((CharP.cast_eq_zero_iff K q 11).1 h11))\n exact orderOf_eq_prime hr11 hr1)\n have := hq.two_le\n omega\n\ntheorem exists_factor (N : ℕ) (hN : N % 11 = 10)\n (hall : ∀ q, q.Prime → q ∣ N → q % 11 = 1 ∨ q % 11 = 10) :\n ∃ q, q.Prime ∧ q % 11 = 10 ∧ q ∣ N :=\n Lemma.RC.exists_factor 11 10 (by decide) (by decide) N hN hall\n\nend Lemma.P1110\n\ntheorem Lemma.primes_mod_11_eq_10 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 11 = 10} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set y := (n + 11).factorial with hydef\n have hy0 : 0 < y := Nat.factorial_pos _\n set x := 11 * y with hxdef\n have hx : 11 ≤ x := by omega\n have hle : x ^ 4 + 4 * x ^ 3 + 1 ≤ x ^ 5 + 3 * x ^ 2 + 3 * x := by\n have e5 : x ^ 5 = x ^ 4 * x := by ring\n have e4 : x ^ 4 = x ^ 3 * x := by ring\n have h3 : 1 ≤ x ^ 3 := Nat.one_le_pow _ _ (by omega)\n have h4 : x ^ 3 * 11 ≤ x ^ 3 * x := Nat.mul_le_mul_left _ hx\n have h5 : x ^ 4 * 11 ≤ x ^ 4 * x := Nat.mul_le_mul_left _ hx\n nlinarith\n set N := x ^ 5 + 3 * x ^ 2 + 3 * x - (x ^ 4 + 4 * x ^ 3 + 1) with hNdef\n have hN : N + (x ^ 4 + 4 * x ^ 3 + 1) = x ^ 5 + 3 * x ^ 2 + 3 * x := Nat.sub_add_cancel hle\n have hN' : N + (14641 * y ^ 4 + 5324 * y ^ 3 + 1) = 161051 * y ^ 5 + 363 * y ^ 2 + 33 * y := by\n rw [hxdef] at hN; linarith [hN]\n have hN11 : N % 11 = 10 := by\n generalize y ^ 5 = a at hN'\n generalize y ^ 4 = b at hN'\n generalize y ^ 3 = c at hN'\n generalize y ^ 2 = d at hN'\n omega\n have hfac : ∀ q, q.Prime → q ∣ N → (q % 11 = 1 ∨ q % 11 = 10) ∧ ¬ q ∣ y := by\n intro q hq hqN\n haveI := Fact.mk hq\n have hc : ((N : ℕ) : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqN\n have hc2 : ((N + (x ^ 4 + 4 * x ^ 3 + 1) : ℕ) : ZMod q)\n = ((x ^ 5 + 3 * x ^ 2 + 3 * x : ℕ) : ZMod q) := by rw [hN]\n push_cast at hc2\n rw [hc] at hc2\n have hf : (-(x : ZMod q)) ^ 5 + (-(x : ZMod q)) ^ 4 - 4 * (-(x : ZMod q)) ^ 3\n - 3 * (-(x : ZMod q)) ^ 2 + 3 * (-(x : ZMod q)) + 1 = 0 := by\n linear_combination hc2\n have hny : ¬ q ∣ y := by\n intro hqy\n have : (x : ZMod q) = 0 := by\n rw [hxdef]; push_cast\n rw [(CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy, mul_zero]\n rw [this] at hf\n norm_num at hf\n refine ⟨Lemma.P1110.key q hq ?_ _ hf, hny⟩\n rintro rfl\n have := Nat.mod_eq_zero_of_dvd hqN\n omega\n obtain ⟨q, hq, h10, hqd⟩ :=\n Lemma.P1110.exists_factor N hN11 (fun q hq hd => (hfac q hq hd).1)\n refine ⟨q, ⟨hq, h10⟩, ?_⟩\n by_contra hle'\n push_neg at hle'\n exact (hfac q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n\n-- U160 generic real_cyc\n-- run2\n","Lemma.primes_mod_12_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P121\n\ntheorem key (x N : ℕ) (hx : 6 ∣ x) (hN : N + x ^ 2 = x ^ 4 + 1) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ N) : q % 12 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 3) := Fact.mk Nat.prime_three\n have hN0 : ((N : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n have hNc : ((N : ℕ) : ZMod q) + (x : ZMod q) ^ 2 = (x : ZMod q) ^ 4 + 1 := by\n have := congrArg (fun m : ℕ => (m : ZMod q)) hN\n push_cast at this\n exact this\n have h1 : (x : ZMod q) ^ 4 + 1 = (x : ZMod q) ^ 2 := by\n linear_combination -hNc + hN0\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 hq2 : q ≠ 2 := by\n rintro rfl\n obtain ⟨k, rfl⟩ := hx\n have e1 : (6 * k) ^ 2 = 2 * (18 * k ^ 2) := by ring\n have e2 : (6 * k) ^ 4 = 2 * (648 * k ^ 4) := by ring\n rw [e1, e2] at hN\n have := Nat.mod_eq_zero_of_dvd hd\n omega\n set u : ZMod q := -(x : ZMod q) ^ 2 with hudef\n have hu3 : u ^ 3 = 1 := by\n rw [hudef]\n linear_combination (-((x : ZMod q) ^ 2 + 1)) * h1\n have hu1 : u ≠ 1 := by\n intro hu\n rw [hudef] at hu\n have h3 : ((3 : ℕ) : ZMod q) = 0 := by\n push_cast\n linear_combination h1 + ((x : ZMod q) ^ 2 - 2) * hu\n have hq3 : q ∣ 3 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n have : q = 3 := (Nat.prime_dvd_prime_iff_eq hq Nat.prime_three).1 hq3\n exact hndvd (this ▸ (Dvd.dvd.trans (by norm_num : 3 ∣ 6) hx))\n have hu0 : u ≠ 0 := by\n rw [hudef]\n exact neg_ne_zero.mpr (pow_ne_zero 2 hx0)\n have hord : orderOf u = 3 := orderOf_eq_prime hu3 hu1\n have hdvd : 3 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hu0\n have hinv : (x : ZMod q) * (x : ZMod q)⁻¹ = 1 := mul_inv_cancel₀ hx0\n have hsq : IsSquare (-1 : ZMod q) :=\n ⟨((x : ZMod q) ^ 2 - 1) * (x : ZMod q)⁻¹, by\n linear_combination (-((x : ZMod q)⁻¹) ^ 2) * h1\n + ((x : ZMod q) * (x : ZMod q)⁻¹ + 1) * hinv⟩\n have h4 := (ZMod.exists_sq_eq_neg_one_iff (p := q)).1 hsq\n have hodd := hq.eq_two_or_odd\n have h2 := hq.two_le\n omega\n\nend Lemma.P121\n\ntheorem Lemma.primes_mod_12_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 12 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 6).factorial with hxdef\n have hx6 : 6 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hxpos : 0 < x := Nat.factorial_pos _\n have hx2 : 2 ≤ x := by\n have : (6 : ℕ) ≤ x := Nat.le_of_dvd hxpos hx6\n omega\n have hx4 : 4 ≤ x ^ 2 := by nlinarith\n have h4 : x ^ 4 = x ^ 2 * x ^ 2 := by ring\n have hle : x ^ 2 ≤ x ^ 4 + 1 := by\n rw [h4]\n have := Nat.mul_le_mul_left (x ^ 2) hx4\n omega\n set N := x ^ 4 + 1 - x ^ 2 with hNdef\n have hN : N + x ^ 2 = x ^ 4 + 1 := Nat.sub_add_cancel hle\n have hN1 : N ≠ 1 := by\n have hm : x ^ 2 * 4 ≤ x ^ 2 * x ^ 2 := Nat.mul_le_mul_left _ hx4\n rw [h4] at hN\n generalize x ^ 2 * x ^ 2 = b at *\n generalize x ^ 2 = a at *\n omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n obtain ⟨h12, hnd⟩ := Lemma.P121.key x N hx6 hN _ hq hqd\n refine ⟨_, ⟨hq, h12⟩, ?_⟩\n by_contra hle'\n push_neg at hle'\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n","Lemma.primes_mod_12_eq_11":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P1211\n\ntheorem z3 : (3 : ZMod 3) = 0 := by decide\n\ntheorem nsq2 : ∀ r : ZMod 3, ((2 : ℕ) : ZMod 3) ≠ r * r := by decide\n\ntheorem sq1 : IsSquare ((1 : ℕ) : ZMod 3) := ⟨1, by decide⟩\n\ntheorem prime_three' : Nat.Prime 3 := by decide\n\ntheorem key (y : ℕ) (hy : 2 ∣ y) (hy0 : 0 < y) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ 3 * y ^ 2 - 1) : (q % 12 = 1 ∨ q % 12 = 11) ∧ ¬ q ∣ y := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 3) := Fact.mk prime_three'\n have h1 : ((3 * y ^ 2 - 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n have h5 : 1 ≤ 3 * y ^ 2 := by\n have : 1 ≤ y ^ 2 := Nat.one_le_pow _ _ hy0\n omega\n have h2 : (3 : 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 hq3 : q ≠ 3 := by\n rintro rfl\n have : (3 : ZMod 3) = 0 := z3\n rw [this] at h2\n simp at h2\n have hsq : IsSquare ((3 : ℕ) : ZMod q) := ⟨3 * y, by push_cast; linear_combination (-3) * h2⟩\n have hodd := hq.eq_two_or_odd\n have hq30 : q % 3 ≠ 0 := by\n intro h0\n exact hq3 ((Nat.prime_dvd_prime_iff_eq prime_three' hq).1\n (Nat.dvd_of_mod_eq_zero h0)).symm\n have hlt3 := Nat.mod_lt q (by norm_num : 3 > 0)\n rcases hodd with h | hodd\n · exact absurd h hq2\n have h4 : q % 4 = 1 ∨ q % 4 = 3 := by omega\n rcases h4 with h4 | h4\n · obtain ⟨r, hr⟩ :=\n (ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one (p := q) (q := 3) h4 (by norm_num)).1 hsq\n rw [← ZMod.natCast_mod q 3] at hr\n have : q % 3 ≠ 2 := by\n intro h32\n rw [h32] at hr\n exact nsq2 r hr\n left; omega\n · have hns : ¬ IsSquare ((q : ℕ) : ZMod 3) := fun hh =>\n (ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_three (p := 3) (q := q) (by norm_num) h4\n (Ne.symm hq3)).1 hh hsq\n rw [← ZMod.natCast_mod q 3] at hns\n have : q % 3 ≠ 1 := by\n intro h31\n rw [h31] at hns\n exact hns sq1\n right; omega\n\ntheorem exists11 (N : ℕ) (hN : N % 12 = 11)\n (hf : ∀ q, q.Prime → q ∣ N → q % 12 = 1 ∨ q % 12 = 11) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 12 = 11 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 12 = 11 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, h⟩\n\nend Lemma.P1211\n\ntheorem Lemma.primes_mod_12_eq_11 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 12 = 11} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n have hy2 : 2 ∣ (n + 3).factorial := Nat.dvd_factorial (by norm_num) (by omega)\n have hy0 : 0 < (n + 3).factorial := Nat.factorial_pos _\n have hN : (3 * (n + 3).factorial ^ 2 - 1) % 12 = 11 := by\n obtain ⟨k, hk⟩ := hy2\n have hz : (n + 3).factorial ^ 2 = 4 * k ^ 2 := by rw [hk]; ring\n have : 1 ≤ (n + 3).factorial ^ 2 := Nat.one_le_pow _ _ hy0\n rw [hz] at this ⊢\n omega\n obtain ⟨q, hq, hqd, hq4⟩ := Lemma.P1211.exists11 _ hN\n (fun q hq hd => (Lemma.P1211.key _ hy2 hy0 q hq hd).1)\n refine ⟨q, ⟨hq, hq4⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P1211.key _ hy2 hy0 q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n","Lemma.primes_mod_12_eq_5":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P125\n\ndef P (n : ℕ) : ℕ := ∏ i ∈ Finset.range n, (6 * i + 5)\n\ntheorem P_mod (n : ℕ) : P n % 6 = 1 ∨ P n % 6 = 5 := by\n unfold P\n apply Finset.prod_induction _ (fun x => x % 6 = 1 ∨ x % 6 = 5)\n · intro a b ha hb\n rcases ha with ha | ha <;> rcases hb with hb | hb <;> (rw [Nat.mul_mod, ha, hb]; omega)\n · left; rfl\n · intro i _; omega\n\ntheorem P_sq (n : ℕ) : P n ^ 2 % 12 = 1 := by\n have h := P_mod n\n have h12 : P n % 12 = 1 ∨ P n % 12 = 5 ∨ P n % 12 = 7 ∨ P n % 12 = 11 := by omega\n rw [Nat.pow_mod]\n rcases h12 with h12 | h12 | h12 | h12 <;> rw [h12]\n\ntheorem dvd_P (n q : ℕ) (hq : q % 6 = 5) (hle : q ≤ n) : q ∣ P n := by\n unfold P\n have hmem : q / 6 ∈ Finset.range n := Finset.mem_range.2 (by omega)\n have := Finset.dvd_prod_of_mem (fun i => 6 * i + 5) hmem\n have he : 6 * (q / 6) + 5 = q := by omega\n simpa [he] using this\n\ntheorem key (x : ℕ) (hx : 2 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 2 + 1) : q % 4 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two\n have h1 : ((x ^ 2 + 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 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 : (2 * k) ^ 2 + 1 = 2 * (2 * k ^ 2) + 1 := by ring\n rw [this]\n omega\n have hn : ¬ (x : ZMod q) ^ (2 ^ 1) = 1 := by\n intro h\n have h2 : ((2 : ℕ) : ZMod q) = 0 := by\n push_cast\n have : (x : ZMod q) ^ 2 = 1 := by simpa using h\n linear_combination h1 - this\n have hq2' : q ∣ 2 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h2\n exact hq2 ((Nat.prime_dvd_prime_iff_eq hq Nat.prime_two).1 hq2')\n have h8 : (x : ZMod q) ^ (2 ^ (1 + 1)) = 1 := by\n norm_num\n linear_combination ((x : ZMod q) ^ 2 - 1) * h1\n have hord : orderOf (x : ZMod q) = 2 ^ (1 + 1) := orderOf_eq_prime_pow hn h8\n have hdvd : 2 ^ (1 + 1) ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have h2 := hq.two_le\n norm_num at hdvd\n omega\n\ntheorem existsA (N : ℕ) (hN : N % 12 = 5)\n (hf : ∀ q, q.Prime → q ∣ N → q % 12 = 1 ∨ q % 12 = 5) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 12 = 5 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 12 = 5 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, h⟩\n\nend Lemma.P125\n\ntheorem Lemma.primes_mod_12_eq_5 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 12 = 5} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := 2 * Lemma.P125.P n with hxdef\n have hx2 : 2 ∣ x := Dvd.intro _ rfl\n have hsq := Lemma.P125.P_sq n\n have hN : (x ^ 2 + 1) % 12 = 5 := by\n have : x ^ 2 + 1 = 4 * Lemma.P125.P n ^ 2 + 1 := by rw [hxdef]; ring\n rw [this]; omega\n obtain ⟨q, hq, hqd, hq5⟩ := Lemma.P125.existsA _ hN (fun q hq hd => by\n have h4 := (Lemma.P125.key x hx2 q hq hd).1\n have h3 : q % 3 ≠ 0 := by\n intro h0\n have h3q : 3 ∣ q := Nat.dvd_of_mod_eq_zero h0\n have : q = 3 := ((Nat.prime_dvd_prime_iff_eq Nat.prime_three hq).1 h3q).symm\n subst this\n have := Nat.mod_eq_zero_of_dvd hd\n omega\n omega)\n refine ⟨q, ⟨hq, hq5⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P125.key x hx2 q hq hqd).2\n (Dvd.dvd.mul_left (Lemma.P125.dvd_P n q (by omega) hle) 2)\n","Lemma.primes_mod_12_eq_7":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P127\n\ndef Q (n : ℕ) : ℕ := ∏ i ∈ Finset.range n, (2 * i + 1)\n\ntheorem Q_odd (n : ℕ) : Q n % 2 = 1 := by\n unfold Q\n apply Finset.prod_induction _ (fun x => x % 2 = 1)\n · intro a b ha hb; rw [Nat.mul_mod, ha, hb]\n · rfl\n · intro i _; omega\n\ntheorem dvd_Q (n q : ℕ) (hq : q % 2 = 1) (hle : q ≤ n) : q ∣ Q n := by\n unfold Q\n have hmem : q / 2 ∈ Finset.range n := Finset.mem_range.2 (by omega)\n have := Finset.dvd_prod_of_mem (fun i => 2 * i + 1) hmem\n have he : 2 * (q / 2) + 1 = q := by omega\n simpa [he] using this\n\ntheorem key (x : ℕ) (hx : 6 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 2 + x + 1) : q % 6 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 3) := Fact.mk Nat.prime_three\n have h1 : ((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 : ((3 : ℕ) : ZMod q) = 0 := by push_cast; linear_combination h1\n have hq3 : q ∣ 3 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n have : q = 3 := (Nat.prime_dvd_prime_iff_eq hq Nat.prime_three).1 hq3\n exact hndvd (this ▸ (Dvd.dvd.trans (by norm_num : 3 ∣ 6) hx))\n have hx3 : (x : ZMod q) ^ 3 = 1 := by\n linear_combination ((x : ZMod q) - 1) * h1\n have hord : orderOf (x : ZMod q) = 3 := orderOf_eq_prime hx3 hx1\n have hdvd : 3 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\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 : (6 * k) ^ 2 + 6 * k + 1 = 2 * (18 * k ^ 2 + 3 * k) + 1 := by ring\n rw [this]\n omega\n have h2 := hq.two_le\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\ntheorem existsA (N : ℕ) (hN : N % 12 = 7)\n (hf : ∀ q, q.Prime → q ∣ N → q % 12 = 1 ∨ q % 12 = 7) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 12 = 7 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 12 = 7 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, h⟩\n\nend Lemma.P127\n\ntheorem Lemma.primes_mod_12_eq_7 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 12 = 7} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := 6 * Lemma.P127.Q n with hxdef\n have hx6 : 6 ∣ x := Dvd.intro _ rfl\n have hodd := Lemma.P127.Q_odd n\n obtain ⟨k, hk⟩ : ∃ k, x = 12 * k + 6 := ⟨Lemma.P127.Q n / 2, by omega⟩\n have hN : (x ^ 2 + x + 1) % 12 = 7 := by\n have : x ^ 2 + x + 1 = 12 * (12 * k ^ 2 + 13 * k + 3) + 7 := by rw [hk]; ring\n rw [this]; omega\n obtain ⟨q, hq, hqd, hq7⟩ := Lemma.P127.existsA _ hN (fun q hq hd => by\n have := (Lemma.P127.key x hx6 q hq hd).1\n have h2 : q % 2 = 1 := by\n rcases hq.eq_two_or_odd with h | h\n · omega\n · exact h\n omega)\n refine ⟨q, ⟨hq, hq7⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P127.key x hx6 q hq hqd).2\n (Dvd.dvd.mul_left (Lemma.P127.dvd_Q n q (by omega) hle) 6)\n","Lemma.primes_mod_3_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P31\n\ntheorem key (x : ℕ) (hx : 6 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 2 + x + 1) : q % 6 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 3) := Fact.mk Nat.prime_three\n have h1 : ((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 : ((3 : ℕ) : ZMod q) = 0 := by push_cast; linear_combination h1\n have hq3 : q ∣ 3 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n have : q = 3 := (Nat.prime_dvd_prime_iff_eq hq Nat.prime_three).1 hq3\n exact hndvd (this ▸ (Dvd.dvd.trans (by norm_num : 3 ∣ 6) hx))\n have hx3 : (x : ZMod q) ^ 3 = 1 := by\n linear_combination ((x : ZMod q) - 1) * h1\n have hord : orderOf (x : ZMod q) = 3 := orderOf_eq_prime hx3 hx1\n have hdvd : 3 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\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 : (6 * k) ^ 2 + 6 * k + 1 = 2 * (18 * k ^ 2 + 3 * k) + 1 := by ring\n rw [this]\n omega\n have h2 := hq.two_le\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.P31\n\ntheorem Lemma.primes_mod_3_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 3 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 3).factorial with hxdef\n have hx6 : 6 ∣ x := by\n have : (3 : ℕ).factorial ∣ x := Nat.factorial_dvd_factorial (by omega)\n simpa [Nat.factorial] using this\n have hN : 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 ^ 2 + x + 1)\n obtain ⟨h6, hnd⟩ := Lemma.P31.key x hx6 _ hq hqd\n refine ⟨_, ⟨hq, by omega⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n","Lemma.primes_mod_3_eq_2":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P32\n\ntheorem exists_factor (N : ℕ) (hN : N % 6 = 5) :\n ∃ q, q.Prime ∧ q % 6 = 5 ∧ q ∣ N := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n set q := N.minFac with hqdef\n have hq2 : q % 2 = 1 := by\n by_contra h\n have h2 : 2 ∣ q := by omega\n have : q = 2 := ((Nat.prime_dvd_prime_iff_eq Nat.prime_two hq).1 h2).symm\n rw [this] at hqd\n omega\n have hq3 : q % 3 ≠ 0 := by\n intro h\n have h3 : 3 ∣ q := by omega\n have : q = 3 := ((Nat.prime_dvd_prime_iff_eq Nat.prime_three hq).1 h3).symm\n rw [this] at hqd\n omega\n by_cases h5 : q % 6 = 5\n · exact ⟨q, hq, h5, hqd⟩\n · have h1 : q % 6 = 1 := by omega\n obtain ⟨m, hm⟩ := hqd\n have hmod := Nat.mul_mod q m 6\n rw [h1, ← hm, hN] at hmod\n have hm5 : m % 6 = 5 := by omega\n have hq2' := hq.two_le\n have hmlt : m < N := by\n have hm0 : 0 < m := by\n apply Nat.pos_of_ne_zero\n rintro rfl\n rw [mul_zero] at hm\n omega\n rw [hm]\n calc m = 1 * m := (one_mul m).symm\n _ < q * m := Nat.mul_lt_mul_of_pos_right hq.one_lt hm0\n obtain ⟨r, hr, hr5, hrd⟩ := ih m hmlt hm5\n exact ⟨r, hr, hr5, hrd.trans ⟨q, by rw [hm, mul_comm]⟩⟩\n\nend Lemma.P32\n\ntheorem Lemma.primes_mod_3_eq_2 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 3 = 2} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 3).factorial with hxdef\n have hx0 : 0 < x := Nat.factorial_pos _\n obtain ⟨q, hq, h5, hd⟩ := Lemma.P32.exists_factor (6 * x - 1) (by omega)\n refine ⟨q, ⟨hq, by omega⟩, ?_⟩\n by_contra hle\n push_neg at hle\n have hqx : q ∣ 6 * x := Dvd.dvd.mul_left (Nat.dvd_factorial hq.pos (by omega)) 6\n have h1 : q ∣ 6 * x - (6 * x - 1) := Nat.dvd_sub hqx hd\n have : 6 * x - (6 * x - 1) = 1 := by omega\n rw [this] at h1\n exact hq.one_lt.ne' (Nat.dvd_one.1 h1)\n","Lemma.primes_mod_4_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P41\n\ntheorem key (x : ℕ) (hx : 2 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 2 + 1) : q % 4 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two\n have h1 : ((x ^ 2 + 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 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 : (2 * k) ^ 2 + 1 = 2 * (2 * k ^ 2) + 1 := by ring\n rw [this]\n omega\n have hn : ¬ (x : ZMod q) ^ (2 ^ 1) = 1 := by\n intro h\n have h2 : ((2 : ℕ) : ZMod q) = 0 := by\n push_cast\n have : (x : ZMod q) ^ 2 = 1 := by simpa using h\n linear_combination h1 - this\n have hq2' : q ∣ 2 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h2\n exact hq2 ((Nat.prime_dvd_prime_iff_eq hq Nat.prime_two).1 hq2')\n have h8 : (x : ZMod q) ^ (2 ^ (1 + 1)) = 1 := by\n norm_num\n linear_combination ((x : ZMod q) ^ 2 - 1) * h1\n have hord : orderOf (x : ZMod q) = 2 ^ (1 + 1) := orderOf_eq_prime_pow hn h8\n have hdvd : 2 ^ (1 + 1) ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have h2 := hq.two_le\n norm_num at hdvd\n omega\n\nend Lemma.P41\n\ntheorem Lemma.primes_mod_4_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 4 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 2).factorial with hxdef\n have hx2 : 2 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hN : x ^ 2 + 1 ≠ 1 := by\n have : 0 < x := Nat.factorial_pos _\n have : 0 < x ^ 2 := by positivity\n omega\n have hq := Nat.minFac_prime hN\n have hqd := Nat.minFac_dvd (x ^ 2 + 1)\n obtain ⟨h8, hnd⟩ := Lemma.P41.key x hx2 _ hq hqd\n refine ⟨_, ⟨hq, h8⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n","Lemma.primes_mod_4_eq_3":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P43\n\ntheorem exists_factor (N : ℕ) (hN : N % 4 = 3) :\n ∃ q, q.Prime ∧ q % 4 = 3 ∧ q ∣ N := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n set q := N.minFac with hqdef\n have hq2 : q % 2 = 1 := by\n by_contra h\n have h2 : 2 ∣ q := by omega\n have : q = 2 := ((Nat.prime_dvd_prime_iff_eq Nat.prime_two hq).1 h2).symm\n rw [this] at hqd\n omega\n by_cases h5 : q % 4 = 3\n · exact ⟨q, hq, h5, hqd⟩\n · have h1 : q % 4 = 1 := by omega\n obtain ⟨m, hm⟩ := hqd\n have hmod := Nat.mul_mod q m 4\n rw [h1, ← hm, hN] at hmod\n have hm5 : m % 4 = 3 := by omega\n have hq2' := hq.two_le\n have hmlt : m < N := by\n have hm0 : 0 < m := by\n apply Nat.pos_of_ne_zero\n rintro rfl\n rw [mul_zero] at hm\n omega\n rw [hm]\n calc m = 1 * m := (one_mul m).symm\n _ < q * m := Nat.mul_lt_mul_of_pos_right hq.one_lt hm0\n obtain ⟨r, hr, hr5, hrd⟩ := ih m hmlt hm5\n exact ⟨r, hr, hr5, hrd.trans ⟨q, by rw [hm, mul_comm]⟩⟩\n\nend Lemma.P43\n\ntheorem Lemma.primes_mod_4_eq_3 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 4 = 3} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 3).factorial with hxdef\n have hx0 : 0 < x := Nat.factorial_pos _\n obtain ⟨q, hq, h5, hd⟩ := Lemma.P43.exists_factor (4 * x - 1) (by omega)\n refine ⟨q, ⟨hq, h5⟩, ?_⟩\n by_contra hle\n push_neg at hle\n have hqx : q ∣ 4 * x := Dvd.dvd.mul_left (Nat.dvd_factorial hq.pos (by omega)) 4\n have h1 : q ∣ 4 * x - (4 * x - 1) := Nat.dvd_sub hqx hd\n have : 4 * x - (4 * x - 1) = 1 := by omega\n rw [this] at h1\n exact hq.one_lt.ne' (Nat.dvd_one.1 h1)\n","Lemma.primes_mod_5_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Q51\n\ntheorem prime_p : Nat.Prime 5 := by decide\n\ntheorem key (x : ℕ) (hx : 5 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 4 + x ^ 3 + x ^ 2 + x + 1) : q % 5 = 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 ▸ 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 omega\n\nend Lemma.Q51\n\ntheorem Lemma.primes_mod_5_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 5 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 10).factorial with hxdef\n have hx6 : 5 ∣ 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.Q51.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","Lemma.primes_mod_5_eq_4":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\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\ntheorem exists4 (N : ℕ) (hN : N % 5 = 4)\n (hf : ∀ q, q.Prime → q ∣ N → q % 5 = 1 ∨ q % 5 = 4) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 5 = 4 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 5 = 4 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, h⟩\n\nend Lemma.P54\n\ntheorem Lemma.primes_mod_5_eq_4 :\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.P54.exists4 _ 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","Lemma.primes_mod_6_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P61\n\ntheorem key (x : ℕ) (hx : 6 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 2 + x + 1) : q % 6 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 3) := Fact.mk Nat.prime_three\n have h1 : ((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 : ((3 : ℕ) : ZMod q) = 0 := by push_cast; linear_combination h1\n have hq3 : q ∣ 3 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n have : q = 3 := (Nat.prime_dvd_prime_iff_eq hq Nat.prime_three).1 hq3\n exact hndvd (this ▸ (Dvd.dvd.trans (by norm_num : 3 ∣ 6) hx))\n have hx3 : (x : ZMod q) ^ 3 = 1 := by\n linear_combination ((x : ZMod q) - 1) * h1\n have hord : orderOf (x : ZMod q) = 3 := orderOf_eq_prime hx3 hx1\n have hdvd : 3 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\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 : (6 * k) ^ 2 + 6 * k + 1 = 2 * (18 * k ^ 2 + 3 * k) + 1 := by ring\n rw [this]\n omega\n have h2 := hq.two_le\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.P61\n\ntheorem Lemma.primes_mod_6_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 6 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 3).factorial with hxdef\n have hx6 : 6 ∣ x := by\n have : (3 : ℕ).factorial ∣ x := Nat.factorial_dvd_factorial (by omega)\n simpa [Nat.factorial] using this\n have hN : 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 ^ 2 + x + 1)\n obtain ⟨h6, hnd⟩ := Lemma.P61.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","Lemma.primes_mod_6_eq_5":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P65\n\ntheorem exists_factor (N : ℕ) (hN : N % 6 = 5) :\n ∃ q, q.Prime ∧ q % 6 = 5 ∧ q ∣ N := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n set q := N.minFac with hqdef\n have hq2 : q % 2 = 1 := by\n by_contra h\n have h2 : 2 ∣ q := by omega\n have : q = 2 := ((Nat.prime_dvd_prime_iff_eq Nat.prime_two hq).1 h2).symm\n rw [this] at hqd\n omega\n have hq3 : q % 3 ≠ 0 := by\n intro h\n have h3 : 3 ∣ q := by omega\n have : q = 3 := ((Nat.prime_dvd_prime_iff_eq Nat.prime_three hq).1 h3).symm\n rw [this] at hqd\n omega\n by_cases h5 : q % 6 = 5\n · exact ⟨q, hq, h5, hqd⟩\n · have h1 : q % 6 = 1 := by omega\n obtain ⟨m, hm⟩ := hqd\n have hmod := Nat.mul_mod q m 6\n rw [h1, ← hm, hN] at hmod\n have hm5 : m % 6 = 5 := by omega\n have hq2' := hq.two_le\n have hmlt : m < N := by\n have hm0 : 0 < m := by\n apply Nat.pos_of_ne_zero\n rintro rfl\n rw [mul_zero] at hm\n omega\n rw [hm]\n calc m = 1 * m := (one_mul m).symm\n _ < q * m := Nat.mul_lt_mul_of_pos_right hq.one_lt hm0\n obtain ⟨r, hr, hr5, hrd⟩ := ih m hmlt hm5\n exact ⟨r, hr, hr5, hrd.trans ⟨q, by rw [hm, mul_comm]⟩⟩\n\nend Lemma.P65\n\ntheorem Lemma.primes_mod_6_eq_5 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 6 = 5} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 3).factorial with hxdef\n have hx0 : 0 < x := Nat.factorial_pos _\n obtain ⟨q, hq, h5, hd⟩ := Lemma.P65.exists_factor (6 * x - 1) (by omega)\n refine ⟨q, ⟨hq, h5⟩, ?_⟩\n by_contra hle\n push_neg at hle\n have hqx : q ∣ 6 * x := Dvd.dvd.mul_left (Nat.dvd_factorial hq.pos (by omega)) 6\n have h1 : q ∣ 6 * x - (6 * x - 1) := Nat.dvd_sub hqx hd\n have : 6 * x - (6 * x - 1) = 1 := by omega\n rw [this] at h1\n exact hq.one_lt.ne' (Nat.dvd_one.1 h1)\n","Lemma.primes_mod_7_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Q71\n\ntheorem prime_p : Nat.Prime 7 := by decide\n\ntheorem key (x : ℕ) (hx : 7 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 6 + x ^ 5 + x ^ 4 + x ^ 3 + x ^ 2 + x + 1) : q % 7 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 7) := Fact.mk prime_p\n have h1 : ((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 : ((7 : ℕ) : ZMod q) = 0 := by push_cast; linear_combination h1\n have hq3 : q ∣ 7 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3\n have : q = 7 := (Nat.prime_dvd_prime_iff_eq hq prime_p).1 hq3\n exact hndvd (this ▸ hx)\n have hx3 : (x : ZMod q) ^ 7 = 1 := by\n linear_combination ((x : ZMod q) - 1) * h1\n have hord : orderOf (x : ZMod q) = 7 := orderOf_eq_prime hx3 hx1\n have hdvd : 7 ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have h2 := hq.two_le\n omega\n\nend Lemma.Q71\n\ntheorem Lemma.primes_mod_7_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 7 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 14).factorial with hxdef\n have hx6 : 7 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hN : x ^ 6 + x ^ 5 + 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 ^ 6 + x ^ 5 + x ^ 4 + x ^ 3 + x ^ 2 + x + 1)\n obtain ⟨h6, hnd⟩ := Lemma.Q71.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","Lemma.primes_mod_7_eq_6":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.RC\n\nopen Polynomial\n\n/-- Generic Frobenius step: if every root `r` of `X^2 - t X + 1` in a field extension of\n`ZMod q` has order `m`, then `m ∣ q - 1` or `m ∣ q + 1`. -/\ntheorem frob (q : ℕ) (hq : q.Prime) (t : ZMod q) (m : ℕ)\n (hord : ∀ (K : Type) [Field K] [Algebra (ZMod q) K] [CharP K q] (r : K),\n r ^ 2 - algebraMap (ZMod q) K t * r + 1 = 0 → orderOf r = m) :\n m ∣ q - 1 ∨ m ∣ q + 1 := by\n haveI := Fact.mk hq\n set p : (ZMod q)[X] := X ^ 2 - C t * X + 1 with hpdef\n have hp : p.natDegree = 2 := by rw [hpdef]; compute_degree!\n have hpu : ¬ IsUnit p := by\n intro h\n have := Polynomial.natDegree_eq_zero_of_isUnit h\n omega\n have hp0 : p ≠ 0 := by\n intro h\n rw [h] at hp\n simp at hp\n obtain ⟨g, hg, hgp⟩ := WfDvdMonoid.exists_irreducible_factor hpu hp0\n haveI := Fact.mk hg\n let K := AdjoinRoot g\n let r : K := AdjoinRoot.root g\n have hr0 : aeval r p = 0 := by\n obtain ⟨c, hc⟩ := hgp\n rw [hc, map_mul, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self, zero_mul]\n set T : K := algebraMap (ZMod q) K t with hTdef\n have hr : r ^ 2 - T * r + 1 = 0 := by\n rw [hpdef] at hr0\n simpa [hTdef] using hr0\n haveI : CharP K q := charP_of_injective_algebraMap (algebraMap (ZMod q) K).injective q\n have hord' : orderOf r = m := hord K r hr\n have hTq : T ^ q = T := by rw [hTdef, ← map_pow, ZMod.pow_card]\n have hrne : r ≠ 0 := by\n intro h0\n rw [h0] at hr\n simp at hr\n have hrq : (r ^ q) ^ 2 - T * r ^ q + 1 = 0 := by\n have : (r ^ 2 - T * r + 1) ^ q = 0 := by rw [hr, zero_pow hq.ne_zero]\n rw [add_pow_char, sub_pow_char, mul_pow, hTq, one_pow] at this\n rw [← this]\n ring\n have hprod : (r ^ q - r) * (r ^ q - (T - r)) = 0 := by linear_combination hrq - hr\n have hq2 := hq.two_le\n rw [← hord']\n rcases mul_eq_zero.1 hprod with h | h\n · left\n apply orderOf_dvd_of_pow_eq_one\n have e : r ^ q = r ^ (q - 1) * r := by\n rw [← pow_succ]; congr 1; omega\n have : (r ^ (q - 1) - 1) * r = 0 := by linear_combination e.symm.trans (sub_eq_zero.1 h)\n rcases mul_eq_zero.1 this with h2 | h2\n · exact sub_eq_zero.1 h2\n · exact absurd h2 hrne\n · right\n apply orderOf_dvd_of_pow_eq_one\n rw [pow_succ, sub_eq_zero.1 h]\n linear_combination -hr\n\n/-- Generic Euclid step: if every prime factor of `N` is `1` or `a` mod `m`, and `N ≡ a`,\nthen some prime factor is `a` mod `m`. -/\ntheorem exists_factor (m a : ℕ) (h1 : 1 % m ≠ a) (ha0 : a ≠ 0) (N : ℕ) (hN : N % m = a)\n (hall : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) :\n ∃ q, q.Prime ∧ q % m = a ∧ q ∣ N := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by rintro rfl; exact h1 hN\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n set q := N.minFac with hqdef\n rcases hall q hq hqd with hq1 | hqa\n · obtain ⟨k, hk⟩ := hqd\n have hmod := Nat.mul_mod q k m\n rw [hq1, ← hk, hN, one_mul, Nat.mod_mod] at hmod\n have hk0 : 0 < k := by\n apply Nat.pos_of_ne_zero\n rintro rfl\n rw [mul_zero] at hk\n rw [hk, Nat.zero_mod] at hN\n exact ha0 hN.symm\n have hklt : k < N := by\n rw [hk]\n calc k = 1 * k := (one_mul k).symm\n _ < q * k := Nat.mul_lt_mul_of_pos_right hq.one_lt hk0\n have hall' : ∀ r, r.Prime → r ∣ k → r % m = 1 ∨ r % m = a := fun r hr hrk =>\n hall r hr (hrk.trans ⟨q, by rw [hk, mul_comm]⟩)\n obtain ⟨r, hr, hra, hrd⟩ := ih k hklt hmod.symm hall'\n exact ⟨r, hr, hra, hrd.trans ⟨q, by rw [hk, mul_comm]⟩⟩\n · exact ⟨q, hq, hqa, hqd⟩\n\nend Lemma.RC\n\nnamespace Lemma.P76\n\ntheorem prime7 : Nat.Prime 7 := by decide\n\ntheorem key (q : ℕ) (hq : q.Prime) (hq7 : q ≠ 7) (t : ZMod q)\n (ht : t ^ 3 + t ^ 2 - 2 * t - 1 = 0) : q % 7 = 1 ∨ q % 7 = 6 := by\n haveI : Fact (Nat.Prime 7) := Fact.mk prime7\n have h := Lemma.RC.frob q hq t 7 (by\n intro K _ _ _ r hr\n set T : K := algebraMap (ZMod q) K t with hTdef\n have hT : T ^ 3 + T ^ 2 - 2 * T - 1 = 0 := by\n have := congrArg (algebraMap (ZMod q) K) ht\n simpa [hTdef, map_ofNat] using this\n have hr7 : r ^ 7 = 1 := by\n linear_combination (r - 1) * (r ^ 3 * hT + (1 + r + r * T + r ^ 2 * T + r ^ 2 * T ^ 2\n + r ^ 3 + r ^ 3 * T + r ^ 4) * hr)\n have hr1 : r ≠ 1 := by\n intro h1\n rw [h1] at hr\n have hT2 : T = 2 := by linear_combination -hr\n rw [hT2] at hT\n have h7 : ((7 : ℕ) : K) = 0 := by push_cast; linear_combination hT\n exact hq7 ((Nat.prime_dvd_prime_iff_eq hq prime7).1 ((CharP.cast_eq_zero_iff K q 7).1 h7))\n exact orderOf_eq_prime hr7 hr1)\n have := hq.two_le\n omega\n\ntheorem exists_factor (N : ℕ) (hN : N % 7 = 6)\n (hall : ∀ q, q.Prime → q ∣ N → q % 7 = 1 ∨ q % 7 = 6) :\n ∃ q, q.Prime ∧ q % 7 = 6 ∧ q ∣ N :=\n Lemma.RC.exists_factor 7 6 (by decide) (by decide) N hN hall\n\nend Lemma.P76\n\ntheorem Lemma.primes_mod_7_eq_6 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 7 = 6} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set y := (n + 7).factorial with hydef\n have hy0 : 0 < y := Nat.factorial_pos _\n set x := 7 * y with hxdef\n have hle : 2 * x + 1 ≤ x ^ 3 + x ^ 2 := by\n have : 7 ≤ x := by omega\n nlinarith\n set N := x ^ 3 + x ^ 2 - (2 * x + 1) with hNdef\n have hN : N + (2 * x + 1) = x ^ 3 + x ^ 2 := Nat.sub_add_cancel hle\n have hN' : N + (14 * y + 1) = 343 * y ^ 3 + 49 * y ^ 2 := by\n rw [hxdef] at hN; linarith [hN]\n have hN7 : N % 7 = 6 := by\n generalize y ^ 3 = a at hN'\n generalize y ^ 2 = b at hN'\n omega\n have hfac : ∀ q, q.Prime → q ∣ N → (q % 7 = 1 ∨ q % 7 = 6) ∧ ¬ q ∣ y := by\n intro q hq hqN\n haveI := Fact.mk hq\n have hc : ((N : ℕ) : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqN\n have hc2 : ((N + (2 * x + 1) : ℕ) : ZMod q) = ((x ^ 3 + x ^ 2 : ℕ) : ZMod q) := by rw [hN]\n push_cast at hc2\n rw [hc] at hc2\n have hf : (x : ZMod q) ^ 3 + (x : ZMod q) ^ 2 - 2 * (x : ZMod q) - 1 = 0 := by\n linear_combination -hc2\n have hny : ¬ q ∣ y := by\n intro hqy\n have : (x : ZMod q) = 0 := by\n rw [hxdef]; push_cast\n rw [(CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy, mul_zero]\n rw [this] at hf\n norm_num at hf\n refine ⟨Lemma.P76.key q hq ?_ _ hf, hny⟩\n rintro rfl\n omega\n obtain ⟨q, hq, h6, hqd⟩ := Lemma.P76.exists_factor N hN7 (fun q hq hd => (hfac q hq hd).1)\n refine ⟨q, ⟨hq, h6⟩, ?_⟩\n by_contra hle'\n push_neg at hle'\n exact (hfac q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n\n-- U160 generic real_cyc\n-- run2\n","Lemma.primes_mod_8_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P81\n\ntheorem key (x : ℕ) (hx : 2 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 4 + 1) : q % 8 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two\n have h1 : ((x ^ 4 + 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 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 : (2 * k) ^ 4 + 1 = 2 * (8 * k ^ 4) + 1 := by ring\n rw [this]\n omega\n have hn : ¬ (x : ZMod q) ^ (2 ^ 2) = 1 := by\n intro h\n have h2 : ((2 : ℕ) : ZMod q) = 0 := by\n push_cast\n have : (x : ZMod q) ^ 4 = 1 := by simpa using h\n linear_combination h1 - this\n have hq2' : q ∣ 2 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h2\n exact hq2 ((Nat.prime_dvd_prime_iff_eq hq Nat.prime_two).1 hq2')\n have h8 : (x : ZMod q) ^ (2 ^ (2 + 1)) = 1 := by\n norm_num\n linear_combination ((x : ZMod q) ^ 4 - 1) * h1\n have hord : orderOf (x : ZMod q) = 2 ^ (2 + 1) := orderOf_eq_prime_pow hn h8\n have hdvd : 2 ^ (2 + 1) ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have h2 := hq.two_le\n norm_num at hdvd\n omega\n\nend Lemma.P81\n\ntheorem Lemma.primes_mod_8_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 8 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 2).factorial with hxdef\n have hx2 : 2 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hN : x ^ 4 + 1 ≠ 1 := by\n have : 0 < x := Nat.factorial_pos _\n have : 0 < x ^ 4 := by positivity\n omega\n have hq := Nat.minFac_prime hN\n have hqd := Nat.minFac_dvd (x ^ 4 + 1)\n obtain ⟨h8, hnd⟩ := Lemma.P81.key x hx2 _ hq hqd\n refine ⟨_, ⟨hq, h8⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n","Lemma.primes_mod_8_eq_3":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P83\n\ndef Q (n : ℕ) : ℕ := ∏ i ∈ Finset.range n, (2 * i + 1)\n\ntheorem Q_odd (n : ℕ) : Q n % 2 = 1 := by\n unfold Q\n apply Finset.prod_induction _ (fun x => x % 2 = 1)\n · intro a b ha hb; rw [Nat.mul_mod, ha, hb]\n · rfl\n · intro i _; omega\n\ntheorem Q_pos (n : ℕ) : 0 < Q n := by have := Q_odd n; omega\n\ntheorem Q_sq (n : ℕ) : Q n ^ 2 % 8 = 1 := by\n have h := Q_odd n\n have h8 : Q n % 8 = 1 ∨ Q n % 8 = 3 ∨ Q n % 8 = 5 ∨ Q n % 8 = 7 := by omega\n rw [Nat.pow_mod]\n rcases h8 with h8 | h8 | h8 | h8 <;> rw [h8]\n\ntheorem dvd_Q (n q : ℕ) (hq : q % 2 = 1) (hle : q ≤ n) : q ∣ Q n := by\n unfold Q\n have hmem : q / 2 ∈ Finset.range n := Finset.mem_range.2 (by omega)\n have := Finset.dvd_prod_of_mem (fun i => 2 * i + 1) hmem\n have he : 2 * (q / 2) + 1 = q := by omega\n simpa [he] using this\n\ntheorem key (n q : ℕ) (hq : q.Prime) (hd : q ∣ Q n ^ 2 + 2) :\n (q % 8 = 1 ∨ q % 8 = 3) ∧ ¬ q ∣ Q n := by\n haveI := Fact.mk hq\n have h2 : ((Q n : ℕ) : ZMod q) ^ 2 + 2 = 0 := by\n have := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at this\n exact this\n have hq2 : q ≠ 2 := by\n rintro rfl\n have h := Q_sq n\n have : (Q n ^ 2 + 2) % 2 = 0 := Nat.mod_eq_zero_of_dvd hd\n omega\n have hndvd : ¬ q ∣ Q n := by\n intro hqy\n have hq2' : q ∣ 2 := (Nat.dvd_add_right (dvd_pow hqy two_ne_zero)).1 hd\n exact hq2 ((Nat.prime_dvd_prime_iff_eq hq Nat.prime_two).1 hq2')\n refine ⟨?_, hndvd⟩\n have hsq : IsSquare (-2 : ZMod q) := ⟨(Q n : ZMod q), by linear_combination (-1) * h2⟩\n exact (ZMod.exists_sq_eq_neg_two_iff hq2).1 hsq\n\ntheorem existsA (N : ℕ) (hN : N % 8 = 3)\n (hf : ∀ q, q.Prime → q ∣ N → q % 8 = 1 ∨ q % 8 = 3) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 8 = 3 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 8 = 3 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, h⟩\n\nend Lemma.P83\n\ntheorem Lemma.primes_mod_8_eq_3 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 8 = 3} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n have hN : (Lemma.P83.Q n ^ 2 + 2) % 8 = 3 := by\n have := Lemma.P83.Q_sq n\n omega\n obtain ⟨q, hq, hqd, hq4⟩ := Lemma.P83.existsA _ hN\n (fun q hq hd => (Lemma.P83.key n q hq hd).1)\n refine ⟨q, ⟨hq, hq4⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P83.key n q hq hqd).2 (Lemma.P83.dvd_Q n q (by omega) hle)\n","Lemma.primes_mod_8_eq_5":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P85\n\ndef Q (n : ℕ) : ℕ := ∏ i ∈ Finset.range n, (2 * i + 1)\n\ntheorem Q_odd (n : ℕ) : Q n % 2 = 1 := by\n unfold Q\n apply Finset.prod_induction _ (fun x => x % 2 = 1)\n · intro a b ha hb; rw [Nat.mul_mod, ha, hb]\n · rfl\n · intro i _; omega\n\ntheorem Q_pos (n : ℕ) : 0 < Q n := by have := Q_odd n; omega\n\ntheorem Q_sq (n : ℕ) : Q n ^ 2 % 8 = 1 := by\n have h := Q_odd n\n have h8 : Q n % 8 = 1 ∨ Q n % 8 = 3 ∨ Q n % 8 = 5 ∨ Q n % 8 = 7 := by omega\n rw [Nat.pow_mod]\n rcases h8 with h8 | h8 | h8 | h8 <;> rw [h8]\n\ntheorem dvd_Q (n q : ℕ) (hq : q % 2 = 1) (hle : q ≤ n) : q ∣ Q n := by\n unfold Q\n have hmem : q / 2 ∈ Finset.range n := Finset.mem_range.2 (by omega)\n have := Finset.dvd_prod_of_mem (fun i => 2 * i + 1) hmem\n have he : 2 * (q / 2) + 1 = q := by omega\n simpa [he] using this\n\ntheorem key (n q : ℕ) (hq : q.Prime) (hd : q ∣ 4 * Q n ^ 2 + 1) :\n (q % 8 = 1 ∨ q % 8 = 5) ∧ ¬ q ∣ Q n := by\n haveI := Fact.mk hq\n have h2 : 4 * ((Q n : ℕ) : ZMod q) ^ 2 + 1 = 0 := by\n have := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n push_cast at this\n exact this\n have hq2 : q ≠ 2 := by\n rintro rfl\n have : (4 * Q n ^ 2 + 1) % 2 = 0 := Nat.mod_eq_zero_of_dvd hd\n omega\n have hndvd : ¬ q ∣ Q n := by\n intro hqy\n have : ((Q n : ℕ) : 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 hsq : IsSquare (-1 : ZMod q) := ⟨2 * (Q n : ZMod q), by linear_combination (-1) * h2⟩\n have h4 := (ZMod.exists_sq_eq_neg_one_iff (p := q)).1 hsq\n have hodd := hq.eq_two_or_odd\n omega\n\ntheorem existsA (N : ℕ) (hN : N % 8 = 5)\n (hf : ∀ q, q.Prime → q ∣ N → q % 8 = 1 ∨ q % 8 = 5) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 8 = 5 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 8 = 5 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, h⟩\n\nend Lemma.P85\n\ntheorem Lemma.primes_mod_8_eq_5 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 8 = 5} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n have hN : (4 * Lemma.P85.Q n ^ 2 + 1) % 8 = 5 := by\n have := Lemma.P85.Q_sq n\n omega\n obtain ⟨q, hq, hqd, hq4⟩ := Lemma.P85.existsA _ hN\n (fun q hq hd => (Lemma.P85.key n q hq hd).1)\n refine ⟨q, ⟨hq, hq4⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P85.key n q hq hqd).2 (Lemma.P85.dvd_Q n q (by omega) hle)\n","Lemma.primes_mod_8_eq_7":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P87\n\ntheorem key (y : ℕ) (hy : 2 ∣ y) (hy0 : 0 < y) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ 2 * y ^ 2 - 1) : (q % 8 = 1 ∨ q % 8 = 7) ∧ ¬ q ∣ y := by\n haveI := Fact.mk hq\n have h1 : ((2 * y ^ 2 - 1 : ℕ) : ZMod q) = 0 :=\n (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n have h5 : 1 ≤ 2 * y ^ 2 := by\n have : 1 ≤ y ^ 2 := Nat.one_le_pow _ _ hy0\n omega\n have h2 : (2 : 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 hsq : IsSquare (2 : ZMod q) := ⟨2 * y, by linear_combination (-2) * h2⟩\n exact (ZMod.exists_sq_eq_two_iff hq2).1 hsq\n\ntheorem exists7 (N : ℕ) (hN : N % 8 = 7)\n (hf : ∀ q, q.Prime → q ∣ N → q % 8 = 1 ∨ q % 8 = 7) :\n ∃ q, q.Prime ∧ q ∣ N ∧ q % 8 = 7 := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by omega\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n rcases hf _ hq hqd with h | h\n · obtain ⟨k, hk⟩ := hqd\n have hk5 : k % 8 = 7 := by\n rw [hk, Nat.mul_mod, h] at hN\n omega\n have hklt : k < N := by\n have := hq.two_le\n have hk0 : 0 < k := by omega\n rw [hk]\n nlinarith\n have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n obtain ⟨p, hp, hpd, hp4⟩ :=\n ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n · exact ⟨_, hq, hqd, h⟩\n\nend Lemma.P87\n\ntheorem Lemma.primes_mod_8_eq_7 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 8 = 7} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n have hy2 : 2 ∣ (n + 3).factorial := Nat.dvd_factorial (by norm_num) (by omega)\n have hy0 : 0 < (n + 3).factorial := Nat.factorial_pos _\n have hN : (2 * (n + 3).factorial ^ 2 - 1) % 8 = 7 := by\n obtain ⟨k, hk⟩ := hy2\n have hz : (n + 3).factorial ^ 2 = 4 * k ^ 2 := by rw [hk]; ring\n have : 1 ≤ (n + 3).factorial ^ 2 := Nat.one_le_pow _ _ hy0\n rw [hz] at this ⊢\n omega\n obtain ⟨q, hq, hqd, hq4⟩ := Lemma.P87.exists7 _ hN\n (fun q hq hd => (Lemma.P87.key _ hy2 hy0 q hq hd).1)\n refine ⟨q, ⟨hq, hq4⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact (Lemma.P87.key _ hy2 hy0 q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n","Lemma.primes_mod_9_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P91\n\ntheorem key (x : ℕ) (hx : 3 ∣ x) (q : ℕ) (hq : q.Prime)\n (hd : q ∣ x ^ 6 + x ^ 3 + 1) : q % 9 = 1 ∧ ¬ q ∣ x := by\n haveI := Fact.mk hq\n haveI : Fact (Nat.Prime 3) := Fact.mk Nat.prime_three\n have h1 : ((x ^ 6 + x ^ 3 + 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 hq3 : q ≠ 3 := by\n rintro rfl\n exact hndvd hx\n have hn : ¬ (x : ZMod q) ^ (3 ^ 1) = 1 := by\n intro h\n have h3' : ((3 : ℕ) : ZMod q) = 0 := by\n push_cast\n have h3 : (x : ZMod q) ^ 3 = 1 := by simpa using h\n linear_combination h1 - ((x : ZMod q) ^ 3 + 2) * h3\n have hq3' : q ∣ 3 := (CharP.cast_eq_zero_iff (ZMod q) q _).1 h3'\n exact hq3 ((Nat.prime_dvd_prime_iff_eq hq Nat.prime_three).1 hq3')\n have h9 : (x : ZMod q) ^ (3 ^ (1 + 1)) = 1 := by\n norm_num\n linear_combination ((x : ZMod q) ^ 3 - 1) * h1\n have hord : orderOf (x : ZMod q) = 3 ^ (1 + 1) := orderOf_eq_prime_pow hn h9\n have hdvd : 3 ^ (1 + 1) ∣ q - 1 := hord ▸ ZMod.orderOf_dvd_card_sub_one hx0\n have h2 := hq.two_le\n norm_num at hdvd\n omega\n\nend Lemma.P91\n\ntheorem Lemma.primes_mod_9_eq_1 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 9 = 1} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set x := (n + 3).factorial with hxdef\n have hx3 : 3 ∣ x := Nat.dvd_factorial (by norm_num) (by omega)\n have hN : x ^ 6 + x ^ 3 + 1 ≠ 1 := by\n have : 0 < x := Nat.factorial_pos _\n have : 0 < x ^ 6 := by positivity\n omega\n have hq := Nat.minFac_prime hN\n have hqd := Nat.minFac_dvd (x ^ 6 + x ^ 3 + 1)\n obtain ⟨h9, hnd⟩ := Lemma.P91.key x hx3 _ hq hqd\n refine ⟨_, ⟨hq, h9⟩, ?_⟩\n by_contra hle\n push_neg at hle\n exact hnd (Nat.dvd_factorial hq.pos (by omega))\n","Lemma.primes_mod_9_eq_8":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.RC\n\nopen Polynomial\n\n/-- Generic Frobenius step: if every root `r` of `X^2 - t X + 1` in a field extension of\n`ZMod q` has order `m`, then `m ∣ q - 1` or `m ∣ q + 1`. -/\ntheorem frob (q : ℕ) (hq : q.Prime) (t : ZMod q) (m : ℕ)\n (hord : ∀ (K : Type) [Field K] [Algebra (ZMod q) K] [CharP K q] (r : K),\n r ^ 2 - algebraMap (ZMod q) K t * r + 1 = 0 → orderOf r = m) :\n m ∣ q - 1 ∨ m ∣ q + 1 := by\n haveI := Fact.mk hq\n set p : (ZMod q)[X] := X ^ 2 - C t * X + 1 with hpdef\n have hp : p.natDegree = 2 := by rw [hpdef]; compute_degree!\n have hpu : ¬ IsUnit p := by\n intro h\n have := Polynomial.natDegree_eq_zero_of_isUnit h\n omega\n have hp0 : p ≠ 0 := by\n intro h\n rw [h] at hp\n simp at hp\n obtain ⟨g, hg, hgp⟩ := WfDvdMonoid.exists_irreducible_factor hpu hp0\n haveI := Fact.mk hg\n let K := AdjoinRoot g\n let r : K := AdjoinRoot.root g\n have hr0 : aeval r p = 0 := by\n obtain ⟨c, hc⟩ := hgp\n rw [hc, map_mul, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self, zero_mul]\n set T : K := algebraMap (ZMod q) K t with hTdef\n have hr : r ^ 2 - T * r + 1 = 0 := by\n rw [hpdef] at hr0\n simpa [hTdef] using hr0\n haveI : CharP K q := charP_of_injective_algebraMap (algebraMap (ZMod q) K).injective q\n have hord' : orderOf r = m := hord K r hr\n have hTq : T ^ q = T := by rw [hTdef, ← map_pow, ZMod.pow_card]\n have hrne : r ≠ 0 := by\n intro h0\n rw [h0] at hr\n simp at hr\n have hrq : (r ^ q) ^ 2 - T * r ^ q + 1 = 0 := by\n have : (r ^ 2 - T * r + 1) ^ q = 0 := by rw [hr, zero_pow hq.ne_zero]\n rw [add_pow_char, sub_pow_char, mul_pow, hTq, one_pow] at this\n rw [← this]\n ring\n have hprod : (r ^ q - r) * (r ^ q - (T - r)) = 0 := by linear_combination hrq - hr\n have hq2 := hq.two_le\n rw [← hord']\n rcases mul_eq_zero.1 hprod with h | h\n · left\n apply orderOf_dvd_of_pow_eq_one\n have e : r ^ q = r ^ (q - 1) * r := by\n rw [← pow_succ]; congr 1; omega\n have : (r ^ (q - 1) - 1) * r = 0 := by linear_combination e.symm.trans (sub_eq_zero.1 h)\n rcases mul_eq_zero.1 this with h2 | h2\n · exact sub_eq_zero.1 h2\n · exact absurd h2 hrne\n · right\n apply orderOf_dvd_of_pow_eq_one\n rw [pow_succ, sub_eq_zero.1 h]\n linear_combination -hr\n\n/-- Generic Euclid step: if every prime factor of `N` is `1` or `a` mod `m`, and `N ≡ a`,\nthen some prime factor is `a` mod `m`. -/\ntheorem exists_factor (m a : ℕ) (h1 : 1 % m ≠ a) (ha0 : a ≠ 0) (N : ℕ) (hN : N % m = a)\n (hall : ∀ q, q.Prime → q ∣ N → q % m = 1 ∨ q % m = a) :\n ∃ q, q.Prime ∧ q % m = a ∧ q ∣ N := by\n induction N using Nat.strong_induction_on with\n | _ N ih =>\n have hN1 : N ≠ 1 := by rintro rfl; exact h1 hN\n have hq := Nat.minFac_prime hN1\n have hqd := Nat.minFac_dvd N\n set q := N.minFac with hqdef\n rcases hall q hq hqd with hq1 | hqa\n · obtain ⟨k, hk⟩ := hqd\n have hmod := Nat.mul_mod q k m\n rw [hq1, ← hk, hN, one_mul, Nat.mod_mod] at hmod\n have hk0 : 0 < k := by\n apply Nat.pos_of_ne_zero\n rintro rfl\n rw [mul_zero] at hk\n rw [hk, Nat.zero_mod] at hN\n exact ha0 hN.symm\n have hklt : k < N := by\n rw [hk]\n calc k = 1 * k := (one_mul k).symm\n _ < q * k := Nat.mul_lt_mul_of_pos_right hq.one_lt hk0\n have hall' : ∀ r, r.Prime → r ∣ k → r % m = 1 ∨ r % m = a := fun r hr hrk =>\n hall r hr (hrk.trans ⟨q, by rw [hk, mul_comm]⟩)\n obtain ⟨r, hr, hra, hrd⟩ := ih k hklt hmod.symm hall'\n exact ⟨r, hr, hra, hrd.trans ⟨q, by rw [hk, mul_comm]⟩⟩\n · exact ⟨q, hq, hqa, hqd⟩\n\nend Lemma.RC\n\nnamespace Lemma.P98\n\ntheorem prime3 : Nat.Prime 3 := by decide\n\ntheorem key (q : ℕ) (hq : q.Prime) (hq3 : q ≠ 3) (t : ZMod q)\n (ht : t ^ 3 - 3 * t + 1 = 0) : q % 9 = 1 ∨ q % 9 = 8 := by\n haveI : Fact (Nat.Prime 3) := Fact.mk prime3\n have h := Lemma.RC.frob q hq t 9 (by\n intro K _ _ _ r hr\n set T : K := algebraMap (ZMod q) K t with hTdef\n have hT : T ^ 3 - 3 * T + 1 = 0 := by\n have := congrArg (algebraMap (ZMod q) K) ht\n simpa [hTdef, map_ofNat] using this\n have hphi : r ^ 6 + r ^ 3 + 1 = 0 := by\n linear_combination r ^ 3 * hT\n + (1 + r * T - r ^ 2 + r ^ 2 * T ^ 2 + r ^ 3 * T + r ^ 4) * hr\n have hr3 : ¬ r ^ (3 ^ 1) = 1 := by\n intro h3\n have h3' : r ^ 3 = 1 := by simpa using h3\n have h3K : ((3 : ℕ) : K) = 0 := by\n push_cast\n linear_combination hphi - (r ^ 3 + 2) * h3'\n exact hq3 ((Nat.prime_dvd_prime_iff_eq hq prime3).1 ((CharP.cast_eq_zero_iff K q 3).1 h3K))\n have hr9 : r ^ (3 ^ (1 + 1)) = 1 := by\n norm_num\n linear_combination (r ^ 3 - 1) * hphi\n have hord0 : orderOf r = 3 ^ (1 + 1) := orderOf_eq_prime_pow hr3 hr9\n rw [hord0]; norm_num)\n have := hq.two_le\n omega\n\ntheorem exists_factor (N : ℕ) (hN : N % 9 = 8)\n (hall : ∀ q, q.Prime → q ∣ N → q % 9 = 1 ∨ q % 9 = 8) :\n ∃ q, q.Prime ∧ q % 9 = 8 ∧ q ∣ N :=\n Lemma.RC.exists_factor 9 8 (by decide) (by decide) N hN hall\n\nend Lemma.P98\n\ntheorem Lemma.primes_mod_9_eq_8 :\n Set.Infinite {p : ℕ | p.Prime ∧ p % 9 = 8} := by\n apply Set.infinite_of_forall_exists_gt\n intro n\n set y := (n + 9).factorial with hydef\n have hy0 : 0 < y := Nat.factorial_pos _\n set x := 9 * y with hxdef\n have hle : 3 * x + 1 ≤ x ^ 3 := by\n have hx : 9 ≤ x := by omega\n have e3 : x ^ 3 = x ^ 2 * x := by ring\n have e2 : x ^ 2 = x * x := by ring\n have h2 : x * 9 ≤ x * x := Nat.mul_le_mul_left _ hx\n have h3 : x ^ 2 * 9 ≤ x ^ 2 * x := Nat.mul_le_mul_left _ hx\n nlinarith\n set N := x ^ 3 - (3 * x + 1) with hNdef\n have hN : N + (3 * x + 1) = x ^ 3 := Nat.sub_add_cancel hle\n have hN' : N + (27 * y + 1) = 729 * y ^ 3 := by\n rw [hxdef] at hN; linarith [hN]\n have hN9 : N % 9 = 8 := by\n generalize y ^ 3 = a at hN'\n omega\n have hfac : ∀ q, q.Prime → q ∣ N → (q % 9 = 1 ∨ q % 9 = 8) ∧ ¬ q ∣ y := by\n intro q hq hqN\n haveI := Fact.mk hq\n have hc : ((N : ℕ) : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqN\n have hc2 : ((N + (3 * x + 1) : ℕ) : ZMod q) = ((x ^ 3 : ℕ) : ZMod q) := by rw [hN]\n push_cast at hc2\n rw [hc] at hc2\n have hf : (-(x : ZMod q)) ^ 3 - 3 * (-(x : ZMod q)) + 1 = 0 := by\n linear_combination hc2\n have hny : ¬ q ∣ y := by\n intro hqy\n have : (x : ZMod q) = 0 := by\n rw [hxdef]; push_cast\n rw [(CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy, mul_zero]\n rw [this] at hf\n norm_num at hf\n refine ⟨Lemma.P98.key q hq ?_ _ hf, hny⟩\n rintro rfl\n have := Nat.mod_eq_zero_of_dvd hqN\n omega\n obtain ⟨q, hq, h8, hqd⟩ := Lemma.P98.exists_factor N hN9 (fun q hq hd => (hfac q hq hd).1)\n refine ⟨q, ⟨hq, h8⟩, ?_⟩\n by_contra hle'\n push_neg at hle'\n exact (hfac q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n\n-- U160 generic real_cyc\n-- run2\n"}},"flags":[],"id":116,"lab_check":false,"label":"no-improvement","measured":24.0,"reason":null,"score":24.0,"significance":[],"status":"verified","verdicts":[{"audit":true,"lab":true,"measured":24.0,"node":3,"seed":0}]},"entry":{"body":"One generic Lean lemma can replace the three copy-pasted AdjoinRoot/Frobenius files (7_6, 9_8, 11_10). Each statement then becomes a short instantiation: the polynomial h, the cofactor Q, and the order step. Cold compile time for the three files should drop by at least 30% compared with the verified texts (N137, N205), and each file should get much shorter.\nMethod: Minutes 0-5: load the verified 7_6, 9_8 and 11_10 from best.json. Do one cache-busted check_candidate of the three, adding a trailing comment to each, and record the wall time as the baseline. Minutes 5-35: write a lemma `real_cyc_key (q : ℕ) [Fact q.Prime] (T : ZMod q) (m k : ℕ) (hm : prime power m, given as orderOf hypotheses) (hcof : ∀ r in AdjoinRoot (X^2 - C T*X + 1), Φ_m-poly(r) = r^k*hT + (r^2-T r+1)*Q r) (hT : h(T)=0) (hq : ¬ q ∣ m) : q % m = 1 ∨ q % m = m-1`. It factors out the Frobenius step r^q∈{r, T−r} and the order argument that the three files currently duplicate, and the caller supplies only the identity proved by linear_combination. Minutes 35-50: re-derive 7_6, 9_8 and 11_10 as instantiations, each file self-contained with the lemma pasted in. Then do one cache-busted check of the three and compare with the baseline. Minutes 50-55: post the timings, the file sizes and the lemma statement to chat. Do not submit unless the harness requires it; the score stays 24.\nThreshold: 3 (must reach). Result 24; verified by node #3.\nSubmitter notes (data): U160: 24 valid (the 21 other files are best.json verbatim). 7_6, 9_8 and 11_10 rewritten on top of a shared, pasted-in lemma Lemma.RC.frob (q) (hq : q.Prime) (t : ZMod q) (m) (hord : ∀ (K : Type) [Field K] [Algebra (ZMod q) K] [CharP K q] (r : K), r^2 - algebraMap (ZMod q) K t * r + 1 = 0 → orderOf r = m) : m ∣ q - 1 ∨ m ∣ q + 1. It carries the AdjoinRoot construction, the Frobenius step r^q ∈ {r, T-r} and the order divisibility. Also a shared Lemma.RC.exists_factor (m a) (1 % m ≠ a) (a ≠ 0), the strong induction on minFac. Each caller supplies hT (mapped from ht), the cofactor linear_combination and orderOf_eq_prime or orderOf_eq_prime_pow, then omega. All valid first try. Timing on this node, cache-busted 3-file check_candidate: verified texts 34 s, then 24 s; generic 22 s, then 24 s. No meaningful speedup, since compile time is dominated by loading imports. Hypothesis of a drop of at least 30% is rejected. Size: the instance-specific part is 79–94 lines (key about 30 lines, was about 75), but each self-contained file is 175–190 lines against 155–173 for the originals, because the lemma is pasted in. Submitted only because the harness auto-submits anyway; score stays 24.\nStatement checked: faithful","claim":116,"created":1792131621,"credit":[2],"id":309,"kind":"result","label":"no-improvement","parent":null,"program":"euclid-primes","score":24.0,"title":"Cleared U160 threshold: theorems proved 24","unit":160},"followups":[]}