/- Submission body for Math15Catalog.source04 (formalized). Validated against the task's pinned Challenge.lean and fixed header/footer. The platform supplies the imports and opens namespace Bounty; the first command closes that namespace so the helper declarations retain their ordinary names. The final theorem reopens Bounty, and the platform's footer closes it. The mathematical proof uses no additional axioms. Adapted library material is attributed at its source component; its Apache 2.0 license is included below. -/ end Bounty /- Proof component: GrowthCompatibility -/ section /- The primorial definition and elementary divisibility lemmas below are adapted from Mathlib.NumberTheory.Primorial (Patrick Stevens, Yury Kudryashov, Bhavik Mehta), licensed under Apache 2.0. They are included explicitly because the challenge's fixed imports do not expose that module. -/ open Finset Nat /-- The product of all primes at most `n`. -/ def primorial (n : ℕ) : ℕ := ∏ p ∈ range (n + 1) with p.Prime, p theorem primorial_pos (n : ℕ) : 0 < primorial n := prod_pos fun _p hp ↦ (mem_filter.1 hp).2.pos theorem primorial_dvd_primorial {m n : ℕ} (h : m ≤ n) : primorial m ∣ primorial n := by exact prod_dvd_prod_of_subset _ _ _ (by gcongr) lemma Nat.Prime.dvd_primorial_iff {p n : ℕ} (hp : Prime p) : p ∣ primorial n ↔ p ≤ n := by refine ⟨?_, fun h ↦ dvd_prod_of_mem _ (by grind)⟩ intro h simp only [primorial, hp.prime.dvd_finsetProd_iff, mem_filter, mem_range_succ_iff] at h obtain ⟨q, ⟨hqn, hq⟩, hpq⟩ := h exact (Nat.le_of_dvd hq.pos hpq).trans hqn namespace Bounty.Arithmetic /-- Quarter-interval primes imply the doubling-interval consequence needed in the elementary growth estimate; only finitely many small cases remain. -/ theorem doubling_primes_of_quarter (quarter : ∀ n : ℕ, 26 ≤ n → ∃ p : ℕ, p.Prime ∧ n < p ∧ 4*p < 5*n) (n : ℕ) (hn : n ≠ 0) : ∃ p : ℕ, p.Prime ∧ n < p ∧ p ≤ 2*n := by by_cases hlarge : 26 ≤ n · obtain ⟨p, hp, hnp, hpn⟩ := quarter n hlarge exact ⟨p, hp, hnp, by omega⟩ · have hsmall : ∀ n ∈ Finset.Icc 1 25, ∃ p ∈ Finset.Icc 2 47, Nat.Prime p ∧ n < p ∧ p ≤ 2*n := by decide obtain ⟨p, _, hp, hnp, hpn⟩ := hsmall n (Finset.mem_Icc.mpr ⟨by omega, by omega⟩) exact ⟨p, hp, hnp, hpn⟩ private theorem primorial_cubic_small_portable : ∀ k ∈ Finset.Icc 11 63, k ^ 3 < primorial k := by decide /-- The growth proof needs only this prime-existence input, supplied in the final assembly by the elementary quarter-interval theorem. -/ theorem cubic_lt_primorial_of_quarter (quarter : ∀ n : ℕ, 26 ≤ n → ∃ p : ℕ, p.Prime ∧ n < p ∧ 4*p < 5*n) {k : ℕ} (hk : 11 ≤ k) : k ^ 3 < primorial k := by induction k using Nat.strong_induction_on with | h k ih => by_cases hsmall : k ≤ 63 · exact primorial_cubic_small_portable k (Finset.mem_Icc.mpr ⟨hk, hsmall⟩) · let a := k / 2 have ha : 32 ≤ a := by dsimp [a]; omega have hak : a < k := by dsimp [a]; omega have hka : k ≤ 3 * a := by dsimp [a]; omega have h2a : 2 * a ≤ k := by dsimp [a]; omega obtain ⟨p, hp, hap, hp2a⟩ := doubling_primes_of_quarter quarter a (by omega) have hpk : p ≤ k := hp2a.trans h2a have hcop : Nat.Coprime p (primorial a) := hp.coprime_iff_not_dvd.mpr (by simpa [hp.dvd_primorial_iff] using (not_le.mpr hap)) have hdvd : p * primorial a ∣ primorial k := hcop.mul_dvd_of_dvd_of_dvd (hp.dvd_primorial_iff.mpr hpk) (primorial_dvd_primorial (by omega)) have hmul : p * primorial a ≤ primorial k := Nat.le_of_dvd (primorial_pos k) hdvd have hia : a ^ 3 < primorial a := ih a hak (by omega) calc k ^ 3 ≤ (3 * a) ^ 3 := Nat.pow_le_pow_left hka 3 _ = 27 * a ^ 3 := by ring _ < p * primorial a := by nlinarith _ ≤ primorial k := hmul end Bounty.Arithmetic /-- Multiplying distinct small prime divisors preserves divisibility. -/ theorem primorial_dvd_of_prime_support {m r : ℕ} (h : ∀ p : ℕ, p.Prime → p ≤ m → p ∣ r) : primorial m ∣ r := by unfold primorial apply Finset.prod_primes_dvd · intro p hp exact (Finset.mem_filter.mp hp).2.prime · intro p hp obtain ⟨hpm, hp⟩ := Finset.mem_filter.mp hp exact h p hp (by simpa using hpm) namespace Bounty.Arithmetic private def smallPrimes : Finset ℕ := {2, 3, 5, 7, 11} private theorem prime_ge_thirteen_of_not_small {p : ℕ} (hp : Nat.Prime p) (hnot : p ∉ smallPrimes) : 13 ≤ p := by by_contra hlt have : p ≤ 12 := by omega interval_cases p <;> norm_num at hp <;> norm_num [smallPrimes] at hnot /-- A normalized lower bound for a product of distinct primes. -/ theorem prime_set_product_lower (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) : 2310 * 13 ^ S.card ≤ 13 ^ 5 * ∏ p ∈ S, p := by let A := S ∩ smallPrimes let B := S \ smallPrimes let C := smallPrimes \ S have hcardS : A.card + B.card = S.card := Finset.card_inter_add_card_sdiff _ _ have hcard0 : A.card + C.card = 5 := by simpa [A, C, Finset.inter_comm, smallPrimes] using Finset.card_inter_add_card_sdiff smallPrimes S have hprodS : (∏ p ∈ A, p) * ∏ p ∈ B, p = ∏ p ∈ S, p := Finset.prod_inter_mul_prod_sdiff _ _ _ have hprod0 : (∏ p ∈ A, p) * ∏ p ∈ C, p = 2310 := by simpa [A, C, Finset.inter_comm, smallPrimes] using Finset.prod_inter_mul_prod_sdiff smallPrimes S id have hB : 13 ^ B.card ≤ ∏ p ∈ B, p := by apply Finset.pow_card_le_prod intro p hp have hp' := Finset.mem_sdiff.mp hp exact prime_ge_thirteen_of_not_small (hS p hp'.1) hp'.2 have hC : (∏ p ∈ C, p) ≤ 13 ^ C.card := by apply Finset.prod_le_pow_card intro p hp have hp' : p ∈ smallPrimes := (Finset.mem_sdiff.mp hp).1 simp only [smallPrimes, Finset.mem_insert, Finset.mem_singleton] at hp' omega calc 2310 * 13 ^ S.card = ((∏ p ∈ A, p) * ∏ p ∈ C, p) * 13 ^ (A.card + B.card) := by rw [hprod0, hcardS] _ ≤ ((∏ p ∈ A, p) * 13 ^ C.card) * 13 ^ (A.card + B.card) := by gcongr _ = 13 ^ (A.card + C.card) * ((∏ p ∈ A, p) * 13 ^ B.card) := by simp only [pow_add] ring _ = 13 ^ 5 * ((∏ p ∈ A, p) * 13 ^ B.card) := by rw [hcard0] _ ≤ 13 ^ 5 * ((∏ p ∈ A, p) * ∏ p ∈ B, p) := by gcongr _ = 13 ^ 5 * ∏ p ∈ S, p := by rw [hprodS] /-- Six distinct prime factors force a product at least `30030`, with a factor of at least `13` for every further distinct prime. -/ theorem primeFactors_product_lower {v : ℕ} (hv : 0 < v) (hw : 6 ≤ v.primeFactors.card) : 30030 * 13 ^ (v.primeFactors.card - 6) ≤ v := by have h := prime_set_product_lower v.primeFactors (fun _ hp ↦ Nat.prime_of_mem_primeFactors hp) have hprod : (∏ p ∈ v.primeFactors, p) ≤ v := Nat.le_of_dvd hv (Nat.prod_primeFactors_dvd v) have heq : v.primeFactors.card = 6 + (v.primeFactors.card - 6) := by omega conv_lhs at h => rw [heq, pow_add] norm_num at h nlinarith /-- A uniform estimate for the number of distinct prime factors in the large range. -/ theorem primeFactors_pow_bound {v : ℕ} (hv : 10000 ≤ v) : 2 ^ (10 + 3 * v.primeFactors.card) < v ^ 2 := by by_cases hw : v.primeFactors.card ≤ 5 · have hpow : 2 ^ (10 + 3 * v.primeFactors.card) ≤ 2 ^ 25 := Nat.pow_le_pow_right (by norm_num) (by omega) norm_num at hpow nlinarith · have hlow := primeFactors_product_lower (show 0 < v by omega) (show 6 ≤ v.primeFactors.card by omega) let t := v.primeFactors.card - 6 have hw' : v.primeFactors.card = 6 + t := by dsimp [t]; omega have heq : 2 ^ (10 + 3 * v.primeFactors.card) = 268435456 * 8 ^ t := by rw [hw'] have ha : 10 + 3 * (6 + t) = 28 + 3 * t := by omega rw [ha, pow_add, pow_mul] norm_num have hpow : 8 ^ t ≤ (13 ^ t) ^ 2 := by calc 8 ^ t ≤ 169 ^ t := Nat.pow_le_pow_left (by norm_num) t _ = (13 ^ t) ^ 2 := by rw [← pow_mul, mul_comm t 2, pow_mul]; norm_num have hlowsq := Nat.pow_le_pow_left hlow 2 change (30030 * 13 ^ t) ^ 2 ≤ v ^ 2 at hlowsq rw [mul_pow] at hlowsq norm_num at hlowsq have hpos : 0 < (13 ^ t) ^ 2 := by positivity rw [heq] nlinarith /-- The explicit separation estimate used in the unbounded range. -/ theorem separation_bound_of_quarter (quarter : ∀ n : ℕ, 26 ≤ n → ∃ p : ℕ, p.Prime ∧ n < p ∧ 4*p < 5*n) {v s k : ℕ} (hv : 10000 ≤ v) (hs : 0 < s) (hsv : s < 2 * v) (hdiv : primorial k ∣ s) : 8 * k * 2 ^ v.primeFactors.card < v := by have hv0 : 0 < v := by omega have hk : k ^ 3 < 2 * v := by by_cases hsmall : k ≤ 10 · have hp := Nat.pow_le_pow_left hsmall 3 norm_num at hp omega · exact (cubic_lt_primorial_of_quarter quarter (by omega)).trans_le ((Nat.le_of_dvd hs hdiv).trans hsv.le) have hpf := primeFactors_pow_bound hv have hexp : 10 + 3 * v.primeFactors.card = 10 + v.primeFactors.card * 3 := by omega rw [hexp, pow_add, pow_mul] at hpf norm_num at hpf have hJ : 0 < (2 ^ v.primeFactors.card) ^ 3 := by positivity have hcube : (8 * k * 2 ^ v.primeFactors.card) ^ 3 < v ^ 3 := by calc (8 * k * 2 ^ v.primeFactors.card) ^ 3 = 512 * k ^ 3 * (2 ^ v.primeFactors.card) ^ 3 := by ring _ < 512 * (2 * v) * (2 ^ v.primeFactors.card) ^ 3 := by exact Nat.mul_lt_mul_of_pos_right (Nat.mul_lt_mul_of_pos_left hk (by omega)) hJ _ = (1024 * (2 ^ v.primeFactors.card) ^ 3) * v := by ring _ < v ^ 2 * v := Nat.mul_lt_mul_of_pos_right hpf hv0 _ = v ^ 3 := by ring by_contra hnot have hreverse := Nat.pow_le_pow_left (show v ≤ 8 * k * 2 ^ v.primeFactors.card by omega) 3 omega private theorem add_nine_le_nine_two_pow (t : ℕ) : t + 9 ≤ 9 * 2 ^ t := by induction t with | zero => norm_num | succ t ih => have hp : 0 < 2 ^ t := by positivity simp only [pow_succ] nlinarith /-- The elementary sieve factor can be absorbed in the large-range growth bound. -/ theorem weighted_primeFactors_pow_bound {v : ℕ} (hv : 1100000 ≤ v) : 2 ^ (10 + 3 * v.primeFactors.card) * (v.primeFactors.card + 1) ^ 3 < v ^ 2 := by by_cases hw : v.primeFactors.card ≤ 7 · have hpow : 2 ^ (10 + 3 * v.primeFactors.card) ≤ 2 ^ 31 := Nat.pow_le_pow_right (by norm_num) (by omega) have hcube : (v.primeFactors.card + 1) ^ 3 ≤ 8 ^ 3 := Nat.pow_le_pow_left (by omega) 3 have hmul := Nat.mul_le_mul hpow hcube norm_num at hmul nlinarith · let t := v.primeFactors.card - 8 have hw' : v.primeFactors.card = 8 + t := by dsimp [t]; omega have hw6 : v.primeFactors.card - 6 = 2 + t := by omega have hlow := primeFactors_product_lower (show 0 < v by omega) (show 6 ≤ v.primeFactors.card by omega) rw [hw6, pow_add] at hlow norm_num at hlow have hlow' : 5075070 * 13 ^ t ≤ v := by nlinarith have hlowsq := Nat.pow_le_pow_left hlow' 2 have h169 : (13 ^ t) ^ 2 = 169 ^ t := by rw [← pow_mul, mul_comm t 2, pow_mul] norm_num rw [mul_pow, h169] at hlowsq have hcube : (t + 9) ^ 3 ≤ 729 * 8 ^ t := by have hh := Nat.pow_le_pow_left (add_nine_le_nine_two_pow t) 3 have h8 : (2 ^ t) ^ 3 = 8 ^ t := by rw [← pow_mul, mul_comm t 3, pow_mul] norm_num simpa only [mul_pow, h8, Nat.reducePow] using hh have heq : 2 ^ (10 + 3 * v.primeFactors.card) = 2 ^ 34 * 8 ^ t := by have hexp : 10 + 3 * v.primeFactors.card = 34 + 3 * t := by omega rw [hexp, pow_add, pow_mul] norm_num have h64 : 64 ^ t = 8 ^ t * 8 ^ t := by rw [← mul_pow]; norm_num have hpow : 64 ^ t ≤ 169 ^ t := Nat.pow_le_pow_left (by norm_num) t calc 2 ^ (10 + 3 * v.primeFactors.card) * (v.primeFactors.card + 1) ^ 3 = (2 ^ 34 * 8 ^ t) * (t + 9) ^ 3 := by rw [heq, hw']; congr 2; omega _ ≤ (2 ^ 34 * 8 ^ t) * (729 * 8 ^ t) := Nat.mul_le_mul_left _ hcube _ = (2 ^ 34 * 729) * 64 ^ t := by rw [h64]; ring _ ≤ (2 ^ 34 * 729) * 169 ^ t := Nat.mul_le_mul_left _ hpow _ < 5075070 ^ 2 * 169 ^ t := Nat.mul_lt_mul_of_pos_right (by norm_num) (by positivity) _ ≤ v ^ 2 := hlowsq private theorem separation_from_weighted_bound {v k w : ℕ} (hv : 0 < v) (hk : k ^ 3 < 2 * v) (hweight : 2 ^ (10 + 3 * w) * (w + 1) ^ 3 < v ^ 2) : 8 * k * ((w + 1) * 2 ^ w) < v := by let J := (w + 1) * 2 ^ w have hJ : 0 < J := by dsimp [J]; positivity have hexp : 10 + 3 * w = 10 + w * 3 := by omega rw [hexp, pow_add, pow_mul] at hweight norm_num at hweight have hbound : 1024 * J ^ 3 < v ^ 2 := by dsimp [J] convert hweight using 1; ring have hcube : (8 * k * J) ^ 3 < v ^ 3 := by calc (8 * k * J) ^ 3 = 512 * k ^ 3 * J ^ 3 := by ring _ < 512 * (2 * v) * J ^ 3 := Nat.mul_lt_mul_of_pos_right (Nat.mul_lt_mul_of_pos_left hk (by omega)) (by positivity) _ = (1024 * J ^ 3) * v := by ring _ < v ^ 2 * v := Nat.mul_lt_mul_of_pos_right hbound hv _ = v ^ 3 := by ring by_contra hnot change ¬ 8 * k * J < v at hnot have hreverse := Nat.pow_le_pow_left (show v ≤ 8 * k * J by omega) 3 omega /-- The gap bound `(ω(v)+1)*2^ω(v)` is small enough for the mixed-case argument once the removed speed is at least `60000`. -/ theorem elementary_separation_bound_of_quarter (quarter : ∀ n : ℕ, 26 ≤ n → ∃ p : ℕ, p.Prime ∧ n < p ∧ 4*p < 5*n) {v s k : ℕ} (hv : 60000 ≤ v) (hs : 0 < s) (hsv : s < 2 * v) (hdiv : primorial k ∣ s) : 8 * k * ((v.primeFactors.card + 1) * 2 ^ v.primeFactors.card) < v := by have hv0 : 0 < v := by omega by_cases hlarge : 1100000 ≤ v · have hk : k ^ 3 < 2 * v := by by_cases hsmall : k ≤ 10 · have hp := Nat.pow_le_pow_left hsmall 3 norm_num at hp omega · exact (cubic_lt_primorial_of_quarter quarter (by omega)).trans_le ((Nat.le_of_dvd hs hdiv).trans hsv.le) exact separation_from_weighted_bound hv0 hk (weighted_primeFactors_pow_bound hlarge) · by_cases hmid : 147457 ≤ v · have hk : k ≤ 18 := by by_contra hnot have hdvd := dvd_trans (primorial_dvd_primorial (show 19 ≤ k by omega)) hdiv have hle := Nat.le_of_dvd hs hdvd have hval : primorial 19 = 9699690 := by decide rw [hval] at hle omega have hw : v.primeFactors.card ≤ 7 := by by_contra hnot have hlow := primeFactors_product_lower hv0 (show 6 ≤ v.primeFactors.card by omega) have hp : 13 ^ 2 ≤ 13 ^ (v.primeFactors.card - 6) := Nat.pow_le_pow_right (by norm_num) (by omega) norm_num at hp nlinarith have hp : 2 ^ v.primeFactors.card ≤ 2 ^ 7 := Nat.pow_le_pow_right (by norm_num) hw have hj := Nat.mul_le_mul (show v.primeFactors.card + 1 ≤ 8 by omega) hp have hfinal := Nat.mul_le_mul (Nat.mul_le_mul_left 8 hk) hj norm_num at hfinal omega · have hk : k ≤ 16 := by by_contra hnot have hdvd := dvd_trans (primorial_dvd_primorial (show 17 ≤ k by omega)) hdiv have hle := Nat.le_of_dvd hs hdvd have hval : primorial 17 = 510510 := by decide rw [hval] at hle omega have hw : v.primeFactors.card ≤ 6 := by by_contra hnot have hlow := primeFactors_product_lower hv0 (show 6 ≤ v.primeFactors.card by omega) have hp : 13 ^ 1 ≤ 13 ^ (v.primeFactors.card - 6) := Nat.pow_le_pow_right (by norm_num) (by omega) norm_num at hp nlinarith have hp : 2 ^ v.primeFactors.card ≤ 2 ^ 6 := Nat.pow_le_pow_right (by norm_num) hw have hj := Nat.mul_le_mul (show v.primeFactors.card + 1 ≤ 7 by omega) hp have hfinal := Nat.mul_le_mul (Nat.mul_le_mul_left 8 hk) hj norm_num at hfinal omega end Bounty.Arithmetic /- Additional primorial bounds adapted from Mathlib.NumberTheory.Primorial, Mathlib.Data.Nat.Choose.Dvd (Chris Hughes, Patrick Stevens), and Mathlib.Data.Nat.Prime.Factorial (Leonardo de Moura, Jeremy Avigad, Mario Carneiro), all licensed under Apache 2.0. -/ open Finset Nat theorem primorial_zero : primorial 0 = 1 := by decide theorem primorial_one : primorial 1 = 1 := by decide theorem primorial_two : primorial 2 = 2 := by decide theorem Nat.Prime.dvd_factorial : ∀ {n p : ℕ} (_ : Nat.Prime p), p ∣ n ! ↔ p ≤ n | 0, _, hp => iff_of_false hp.not_dvd_one (not_le_of_gt hp.pos) | n + 1, p, hp => by rw [factorial_succ, hp.dvd_mul, Nat.Prime.dvd_factorial hp] exact ⟨fun h => h.elim (le_of_dvd (succ_pos _)) le_succ_of_le, fun h => (_root_.lt_or_eq_of_le h).elim (Or.inr ∘ le_of_lt_succ) fun h => Or.inl <| by rw [h]⟩ /-- A prime between both summands and their sum divides their binomial coefficient. -/ theorem Nat.Prime.dvd_choose_add {p a b : ℕ} (hp : Nat.Prime p) (hap : a < p) (hbp : b < p) (h : p ≤ a + b) : p ∣ Nat.choose (a+b) a := by have h₁ : p ∣ (a+b)! := hp.dvd_factorial.2 h rw [← Nat.add_choose_mul_factorial_mul_factorial, ← Nat.choose_symm_add, hp.dvd_mul, hp.dvd_mul, hp.dvd_factorial, hp.dvd_factorial] at h₁ exact (h₁.resolve_right hbp.not_ge).resolve_right hap.not_ge theorem primorial_succ {n : ℕ} (hn1 : n ≠ 1) (hn : Odd n) : primorial (n + 1) = primorial n := by refine prod_congr ?_ fun _ _ ↦ rfl rw [range_add_one, filter_insert, ite_eq_right fun h ↦ not_even_iff_odd.2 hn _] exact fun h ↦ h.even_sub_one <| mt succ.inj hn1 theorem primorial_add (m n : ℕ) : primorial (m + n) = primorial m * ∏ p ∈ Ico (m + 1) (m + n + 1) with p.Prime, p := by simp_rw [primorial, ← Ico_zero_eq_range] rw [← prod_union, ← filter_union, Ico_union_Ico_eq_Ico] exacts [Nat.zero_le _, by omega, disjoint_filter_filter <| Ico_disjoint_Ico_consecutive _ _ _] theorem primorial_add_dvd {m n : ℕ} (h : n ≤ m) : primorial (m + n) ∣ primorial m * choose (m + n) m := calc primorial (m + n) = primorial m * ∏ p ∈ Ico (m + 1) (m + n + 1) with p.Prime, p := primorial_add _ _ _ ∣ primorial m * choose (m + n) m := mul_dvd_mul_left _ <| prod_primes_dvd _ (fun _ hk ↦ (mem_filter.1 hk).2.prime) fun p hp ↦ by rw [mem_filter, mem_Ico] at hp exact hp.2.dvd_choose_add hp.1.1 (h.trans_lt (m.lt_succ_self.trans_le hp.1.1)) (Nat.lt_succ_iff.1 hp.1.2) theorem primorial_add_le {m n : ℕ} (h : n ≤ m) : primorial (m + n) ≤ primorial m * choose (m + n) m := le_of_dvd (mul_pos (primorial_pos _) (choose_pos <| Nat.le_add_right _ _)) (primorial_add_dvd h) theorem primorial_lt_four_pow (n : ℕ) (hn : n ≠ 0) : primorial n < 4 ^ n := by induction n using Nat.strong_induction_on with | h n ihn => rcases n with - | n; · grind rcases n.even_or_odd with ⟨m, rfl⟩ | ho · rcases m.eq_zero_or_pos with rfl | hm · decide calc primorial (m + m + 1) = primorial (m + 1 + m) := by rw [add_right_comm] _ ≤ primorial (m + 1) * choose (m + 1 + m) (m + 1) := primorial_add_le m.le_succ _ = primorial (m + 1) * choose (2 * m + 1) m := by rw [choose_symm_add, two_mul, add_right_comm] _ < 4 ^ (m + 1) * 4 ^ m := Nat.mul_lt_mul_of_lt_of_le (ihn _ (by omega) (by omega)) (choose_middle_le_pow _) (by simp) _ ≤ 4 ^ (m + m + 1) := by rw [← pow_add, add_right_comm] · rcases Decidable.eq_or_ne n 1 with rfl | hn · decide · calc primorial (n + 1) = primorial n := primorial_succ hn ho _ < 4 ^ n := ihn n n.lt_succ_self (by grind) _ ≤ 4 ^ (n + 1) := Nat.pow_le_pow_right four_pos n.le_succ theorem primorial_le_four_pow (n : ℕ) : primorial n ≤ 4 ^ n := by obtain rfl | hn := eq_or_ne n 0 · decide · exact (primorial_lt_four_pow n hn).le end /- Proof component: Core -/ section noncomputable section namespace Bounty open Math15.LonelyRunner theorem score_le_ML (V : Finset ℕ) (t : Time) : score V t ≤ ML V := by change score V t ≤ sSup (Set.range (score V)) refine le_csSup ?_ ⟨t, rfl⟩ refine ⟨1 / 2, ?_⟩ rintro _ ⟨s, rfl⟩ by_cases h : V.Nonempty · simp only [score, dite_eq_left h] obtain ⟨v, hv⟩ := h exact (Finset.inf'_le (fun v => distance (v • s)) hv).trans (by simpa [distance] using AddCircle.norm_le_half_period (1 : ℝ) (by norm_num) (x := v • s)) · simp [score, h] theorem ML_le_iff_forall_score_le (V : Finset ℕ) (c : ℝ) : ML V ≤ c ↔ ∀ t : Time, score V t ≤ c := by constructor · exact fun h t => (score_le_ML V t).trans h · intro h exact csSup_le (Set.range_nonempty _) (by rintro _ ⟨t, rfl⟩; exact h t) theorem ML_le_iff_covered (V : Finset ℕ) (hV : V.Nonempty) (c : ℝ) : ML V ≤ c ↔ ∀ t : Time, ∃ v ∈ V, distance (v • t) ≤ c := by rw [ML_le_iff_forall_score_le] simp only [score, dite_eq_left hV, Finset.inf'_le_iff] theorem ML_gt_of_all_distances_gt {V : Finset ℕ} (hV : V.Nonempty) {c : ℝ} {t : Time} (h : ∀ v ∈ V, c < distance (v • t)) : c < ML V := by apply lt_of_not_ge intro hc obtain ⟨v, hv, hh⟩ := (ML_le_iff_covered V hV c).mp hc t exact (not_lt_of_ge hh) (h v hv) theorem mem_modified {n r₁ r₂ w₁ w₂ v : ℕ} : v ∈ modified n r₁ r₂ w₁ w₂ ↔ (1 ≤ v ∧ v ≤ n - 1 ∧ v ≠ r₁ ∧ v ≠ r₂) ∨ v = w₁ ∨ v = w₂ := by simp only [modified, Finset.mem_union, Finset.mem_sdiff, Finset.mem_Icc, Finset.mem_insert, Finset.mem_singleton, not_or] tauto theorem modified_nonempty (n r₁ r₂ w₁ w₂ : ℕ) : (modified n r₁ r₂ w₁ w₂).Nonempty := by exact ⟨w₁, mem_modified.mpr (Or.inr (Or.inl rfl))⟩ theorem modified_positive {n r₁ r₂ w₁ w₂ : ℕ} (hn : 1 ≤ n) (hw₁ : n ≤ w₁) (hw₂ : n ≤ w₂) : Positive (modified n r₁ r₂ w₁ w₂) := by intro v hv rcases mem_modified.mp hv with h | rfl | rfl <;> omega theorem inserted_covers_hole {n r₁ r₂ w₁ w₂ : ℕ} {c : ℝ} {t : Time} (hML : ML (modified n r₁ r₂ w₁ w₂) ≤ c) (hretained : ∀ v : ℕ, 1 ≤ v → v < n → v ≠ r₁ → v ≠ r₂ → c < distance (v • t)) : distance (w₁ • t) ≤ c ∨ distance (w₂ • t) ≤ c := by obtain ⟨v, hv, hd⟩ := (ML_le_iff_covered _ (modified_nonempty n r₁ r₂ w₁ w₂) c).mp hML t rcases mem_modified.mp hv with h | rfl | rfl · have hh := hretained v h.1 (by omega) h.2.2.1 h.2.2.2 exact False.elim ((not_lt_of_ge hd) hh) · exact Or.inl hd · exact Or.inr hd theorem admissible_removals_require_four {n r₁ r₂ : ℕ} (hn : 3 ≤ n) (hr₁ : 1 ≤ r₁) (hr₁n : r₁ < n) (hr₂ : 1 ≤ r₂) (hr₂n : r₂ < n) (hne : r₁ ≠ r₂) (hhalf₁ : n - 1 < 2 * r₁) (hhalf₂ : n - 1 < 2 * r₂) : 4 ≤ n := by omega end Bounty end end /- Proof component: Geometry -/ section noncomputable section namespace Math15.LonelyRunner /-- The score at every time is bounded above by its maximum. -/ theorem geometry_score_le_ML (V : Finset ℕ) (t : Time) : score V t ≤ ML V := by apply le_csSup _ (Set.mem_range_self t) refine ⟨1 / 2, ?_⟩ rintro _ ⟨s, rfl⟩ by_cases h : V.Nonempty · simp only [score, dite_eq_left h] obtain ⟨v, hv⟩ := h exact (Finset.inf'_le (fun v => distance (v • s)) hv).trans (by simpa [distance] using AddCircle.norm_le_half_period (1 : ℝ) (by norm_num) (x := v • s)) · simp [score, h] /-- An upper bound on the maximum means some runner is bad at each time. -/ theorem geometry_exists_distance_le_of_ML_le (V : Finset ℕ) (hV : V.Nonempty) {a : ℝ} (ha : ML V ≤ a) (t : Time) : ∃ v ∈ V, distance (v • t) ≤ a := by obtain ⟨v, hv, heq⟩ := Finset.exists_mem_eq_inf' hV (fun v => distance (v • t)) refine ⟨v, hv, ?_⟩ have h := (geometry_score_le_ML V t).trans ha simpa only [score, dite_eq_left hV, heq] using h /-- The exact distance at the reciprocal of an integral speed. -/ theorem distance_reciprocal (v r : ℕ) : distance (v • ((1 / (r : ℝ) : ℝ) : Time)) = (min (v % r) (r - v % r) : ℕ) / (r : ℝ) := by rw [distance, ← AddCircle.coe_nsmul, nsmul_eq_mul, mul_one_div] simpa using (AddCircle.norm_div_natCast (p := (1 : ℝ)) (m := v) (n := r)) /-- A speed not divisible by `r` stays at least `1/r` away from an integer at the reciprocal time `1/r`. -/ theorem reciprocal_distance_lower_bound (v r : ℕ) (hr : 0 < r) (hvr : ¬ r ∣ v) : 1 / (r : ℝ) ≤ distance (v • ((1 / (r : ℝ) : ℝ) : Time)) := by rw [distance_reciprocal] apply div_le_div_of_nonneg_right _ (by positivity) have hm : v % r ≠ 0 := fun h => hvr (Nat.dvd_of_mod_eq_zero h) have hm' := Nat.mod_lt v hr have : 1 ≤ min (v % r) (r - v % r) := by omega exact_mod_cast this /-- A retained canonical speed cannot be bad at the reciprocal time of a removed upper-half speed. -/ theorem retained_distance_gt (n r v : ℕ) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hvpos : 0 < v) (hvn : v < n) (hvr : v ≠ r) : 1 / (n : ℝ) < distance (v • ((1 / (r : ℝ) : ℝ) : Time)) := by have hnot : ¬ r ∣ v := by intro h exact hvr (Nat.eq_of_dvd_of_lt_two_mul (by omega) h (by omega)) exact (one_div_lt_one_div_of_lt (by exact_mod_cast hr) (by exact_mod_cast hrn)).trans_le (reciprocal_distance_lower_bound v r hr hnot) /-- Each removed upper-half speed divides at least one insertion in a tight modified instance. This is the individual divisibility step. -/ theorem removed_dvd_insertion (n r s A B : ℕ) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hML : ML (modified n r s A B) ≤ 1 / (n : ℝ)) : r ∣ A ∨ r ∣ B := by have hV : (modified n r s A B).Nonempty := by refine ⟨A, ?_⟩ simp [modified] obtain ⟨v, hv, hdist⟩ := geometry_exists_distance_le_of_ML_le _ hV hML ((1 / (r : ℝ) : ℝ) : Time) simp only [modified, Finset.mem_union, Finset.mem_sdiff, Finset.mem_Icc, Finset.mem_insert, Finset.mem_singleton] at hv rcases hv with ⟨⟨hvpos, hvn⟩, hvr⟩ | hvA | hvB · have hgt := retained_distance_gt n r v hr hrn hupper (by omega) (by omega) (by intro h; exact hvr (Or.inl h)) exact False.elim (not_lt_of_ge hdist hgt) · subst v by_cases h : r ∣ A · exact Or.inl h · have hgt := (one_div_lt_one_div_of_lt (a := (r : ℝ)) (b := (n : ℝ)) (by exact_mod_cast hr) (by exact_mod_cast hrn)).trans_le (reciprocal_distance_lower_bound A r hr h) exact False.elim (not_lt_of_ge hdist hgt) · subst v by_cases h : r ∣ B · exact Or.inr h · have hgt := (one_div_lt_one_div_of_lt (a := (r : ℝ)) (b := (n : ℝ)) (by exact_mod_cast hr) (by exact_mod_cast hrn)).trans_le (reciprocal_distance_lower_bound B r hr h) exact False.elim (not_lt_of_ge hdist hgt) /-- Exact rational-time distance in terms of integer remainders. -/ theorem distance_rational_center (v p r : ℕ) : distance (v • (((p : ℝ) / (r : ℝ) : ℝ) : Time)) = (min ((v * p) % r) (r - (v * p) % r) : ℕ) / (r : ℝ) := by rw [distance, ← AddCircle.coe_nsmul, nsmul_eq_mul, ← mul_div_assoc] simpa only [Nat.cast_mul, mul_one, one_mul] using (AddCircle.norm_div_natCast (p := (1 : ℝ)) (m := v * p) (n := r)) /-- Primitive rational centers have the same uniform separation as `1/r`. -/ theorem primitive_center_distance_lower_bound (v p r : ℕ) (hr : 0 < r) (hp : Nat.Coprime p r) (hvr : ¬ r ∣ v) : 1 / (r : ℝ) ≤ distance (v • (((p : ℝ) / (r : ℝ) : ℝ) : Time)) := by rw [distance_rational_center] have hnot : ¬ r ∣ v * p := by simpa only [hp.symm.dvd_mul_right] using hvr have h := reciprocal_distance_lower_bound (v * p) r hr hnot simpa only [distance_reciprocal] using h /-- The reverse triangle inequality gives a quantitative perturbation bound. -/ theorem distance_add_lower_bound (v : ℕ) (t d : Time) : distance (v • t) - (v : ℝ) * distance d ≤ distance (v • (t + d)) := by have h := norm_sub_le (v • (t + d)) (v • d) rw [nsmul_add, add_sub_cancel_right] at h have hd := (norm_nsmul_le (a := d) (n := v)) dsimp [distance] rw [nsmul_add] linarith /-- Around each primitive removed-speed center there is an explicit open interval where all retained speeds are good. -/ theorem retained_good_near_primitive_center (n r p v : ℕ) (d : Time) (hr : 0 < r) (_hrn : r < n) (hupper : n - 1 < 2 * r) (hp : Nat.Coprime p r) (hvpos : 0 < v) (hvn : v < n) (hvr : v ≠ r) (hd : (n - 1 : ℕ) * distance d < 1 / (r : ℝ) - 1 / (n : ℝ)) : 1 / (n : ℝ) < distance (v • ((((p : ℝ) / (r : ℝ) : ℝ) : Time) + d)) := by have hnot : ¬ r ∣ v := by intro h exact hvr (Nat.eq_of_dvd_of_lt_two_mul (by omega) h (by omega)) have hcenter := primitive_center_distance_lower_bound v p r hr hp hnot have hperturb := distance_add_lower_bound v (((p : ℝ) / (r : ℝ) : ℝ) : Time) d have hvreal : (v : ℝ) ≤ (n - 1 : ℕ) := by exact_mod_cast (show v ≤ n - 1 by omega) have hdnonneg : 0 ≤ distance d := norm_nonneg _ have hmul := mul_le_mul_of_nonneg_right hvreal hdnonneg linarith /-- Tightness provides a purely integral necessary condition at every rational time. This can be used for exact obstruction certificates. -/ theorem rational_cover_of_ML_le (V : Finset ℕ) (hV : V.Nonempty) (n p q : ℕ) (hn : 0 < n) (hq : 0 < q) (hML : ML V ≤ 1 / (n : ℝ)) : ∃ v ∈ V, n * min ((v * p) % q) (q - (v * p) % q) ≤ q := by obtain ⟨v, hv, hd⟩ := geometry_exists_distance_le_of_ML_le V hV hML ((((p : ℝ) / (q : ℝ)) : ℝ) : Time) refine ⟨v, hv, ?_⟩ rw [distance_rational_center] at hd have hh := (div_le_div_iff₀ (show 0 < (q : ℝ) by exact_mod_cast hq) (show 0 < (n : ℝ) by exact_mod_cast hn)).mp hd norm_num only [one_mul] at hh rw [mul_comm] at hh exact_mod_cast hh /-- In the uniform primitive-center hole, one of the two insertions must provide the cover. -/ theorem insertion_covers_near_primitive_center (n r s A B p : ℕ) (d : Time) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hp : Nat.Coprime p r) (hML : ML (modified n r s A B) ≤ 1 / (n : ℝ)) (hd : (n - 1 : ℕ) * distance d < 1 / (r : ℝ) - 1 / (n : ℝ)) : distance (A • (((((p : ℝ) / (r : ℝ)) : ℝ) : Time) + d)) ≤ 1 / (n : ℝ) ∨ distance (B • (((((p : ℝ) / (r : ℝ)) : ℝ) : Time) + d)) ≤ 1 / (n : ℝ) := by have hV : (modified n r s A B).Nonempty := by refine ⟨A, ?_⟩ simp [modified] obtain ⟨v, hv, hdist⟩ := geometry_exists_distance_le_of_ML_le _ hV hML (((((p : ℝ) / (r : ℝ)) : ℝ) : Time) + d) simp only [modified, Finset.mem_union, Finset.mem_sdiff, Finset.mem_Icc, Finset.mem_insert, Finset.mem_singleton] at hv rcases hv with ⟨⟨hvpos, hvn⟩, hvr⟩ | hvA | hvB · have hgt := retained_good_near_primitive_center n r p v d hr hrn hupper hp (by omega) (by omega) (by intro h; exact hvr (Or.inl h)) hd exact False.elim (not_lt_of_ge hdist hgt) · exact Or.inl (hvA ▸ hdist) · exact Or.inr (hvB ▸ hdist) /-- The integer rational-time covering condition is also sufficient: continuity extends it from rational times to the whole circle. -/ theorem ML_le_of_rational_cover (V : Finset ℕ) (hV : V.Nonempty) (n : ℕ) (hn : 0 < n) (hcover : ∀ p q : ℕ, 0 < q → ∃ v ∈ V, n * min ((v * p) % q) (q - (v * p) % q) ≤ q) : ML V ≤ 1 / (n : ℝ) := by have hnat (p q : ℕ) (hq : 0 < q) : score V (((p : ℝ) / (q : ℝ) : ℝ) : Time) ≤ 1 / (n : ℝ) := by obtain ⟨v, hv, hb⟩ := hcover p q hq unfold score rw [dite_eq_left hV] apply (Finset.inf'_le (fun v => distance (v • (((p : ℝ) / (q : ℝ) : ℝ) : Time))) hv).trans rw [distance_rational_center] apply (div_le_div_iff₀ (show 0 < (q : ℝ) by exact_mod_cast hq) (show 0 < (n : ℝ) by exact_mod_cast hn)).mpr norm_num only [one_mul] rw [mul_comm] exact_mod_cast hb have hrat (a : ℚ) : score V ((a : ℝ) : Time) ≤ 1 / (n : ℝ) := by rw [Rat.cast_def] obtain ⟨p, hp | hp⟩ := Int.eq_nat_or_neg a.num · rw [hp, Int.cast_natCast] exact hnat p a.den a.den_pos · rw [hp, Int.cast_neg, Int.cast_natCast, neg_div, AddCircle.coe_neg] simpa only [score, smul_neg, distance, norm_neg] using hnat p a.den a.den_pos have hreal (x : ℝ) : score V (x : Time) ≤ 1 / (n : ℝ) := by exact (Rat.denseRange_cast : DenseRange (fun q : ℚ => (q : ℝ))).induction_on x (isClosed_le ((score_continuous V).comp (AddCircle.continuous_mk' (1 : ℝ))) continuous_const) hrat apply csSup_le (Set.range_nonempty _) rintro _ ⟨t, rfl⟩ obtain ⟨x, rfl⟩ := QuotientAddGroup.mk_surjective t exact hreal x /-- A wholly integer criterion equivalent to the analytic maximum bound. -/ theorem ML_le_iff_rational_cover (V : Finset ℕ) (hV : V.Nonempty) (n : ℕ) (hn : 0 < n) : ML V ≤ 1 / (n : ℝ) ↔ ∀ p q : ℕ, 0 < q → ∃ v ∈ V, n * min ((v * p) % q) (q - (v * p) % q) ≤ q := by constructor · intro h p q hq exact rational_cover_of_ML_le V hV n p q hn hq h · exact ML_le_of_rational_cover V hV n hn /-- A point strictly between successive grid intervals is uncovered. -/ theorem between_grid_intervals {s h c x : ℝ} (hs : 0 < s) (k : ℤ) (hl : c + (k : ℝ) * s + h < x) (hr : x < c + (k + 1 : ℤ) * s - h) : ¬ ∃ j : ℤ, |x - (c + (j : ℝ) * s)| ≤ h := by rintro ⟨j, hj⟩ rcases le_or_gt j k with hjk | hjk · have hjk' : (j : ℝ) ≤ (k : ℝ) := by exact_mod_cast hjk have hmul := mul_le_mul_of_nonneg_right hjk' hs.le have habs := (abs_le.mp hj).2 linarith · have hjk' : ((k + 1 : ℤ) : ℝ) ≤ (j : ℝ) := by exact_mod_cast (show k + 1 ≤ j by omega) have hmul := mul_le_mul_of_nonneg_right hjk' hs.le have habs := (abs_le.mp hj).1 linarith /-- A real interval covered by disjoint equally spaced closed intervals can have length at most the length of one covering interval. -/ theorem covered_grid_interval_length {a b c s h : ℝ} (hs : 0 < s) (hgap : 2 * h < s) (hab : a ≤ b) (hcover : ∀ x ∈ Set.Icc a b, ∃ k : ℤ, |x - (c + (k : ℝ) * s)| ≤ h) : b - a ≤ 2 * h := by by_contra! hlong obtain ⟨k, hk⟩ := hcover a ⟨le_rfl, hab⟩ have hklo := (abs_le.mp hk).1 have hkhi := (abs_le.mp hk).2 let e := c + (k : ℝ) * s + h let f := c + ((k + 1 : ℤ) : ℝ) * s - h have he_a : a ≤ e := by dsimp [e]; linarith have he_b : e < b := by dsimp [e]; linarith have he_f : e < f := by dsimp [e, f]; push_cast; linarith let x := (e + min b f) / 2 have he_x : e < x := by dsimp [x]; have := lt_min he_b he_f; linarith have hx_b : x < b := by dsimp [x]; have := min_le_left b f; linarith have hx_f : x < f := by dsimp [x]; have := min_le_right b f; linarith exact between_grid_intervals hs k he_x hx_f (hcover x ⟨le_trans he_a he_x.le, hx_b.le⟩) /-- A component of two families of grid intervals extends to the right of a center of the first family by at most its radius plus the second diameter. -/ theorem two_grid_cover_right_bound {b c P Q hP hQ : ℝ} (hP0 : 0 ≤ hP) (hQ0 : 0 ≤ hQ) (hPgap : 2 * hP + 2 * hQ < P) (hQgap : 2 * hQ < Q) (hcover : ∀ x ∈ Set.Icc 0 b, (∃ k : ℤ, |x - (k : ℝ) * P| ≤ hP) ∨ (∃ j : ℤ, |x - (c + (j : ℝ) * Q)| ≤ hQ)) : b ≤ hP + 2 * hQ := by by_contra! hlong have hPpos : 0 < P := by linarith have hQpos : 0 < Q := by linarith let e := min b (P - hP) have he : hP + 2 * hQ < e := by exact lt_min hlong (by linarith) let d := (e - hP - 2 * hQ) / 3 have hd : 0 < d := by dsimp [d]; linarith let a := hP + d let z := e - d have ha0 : 0 ≤ a := by dsimp [a]; linarith have haz : a ≤ z := by dsimp [a, z, d]; linarith have hz_b : z ≤ b := by dsimp [z]; have := min_le_left b (P - hP); change e ≤ b at this; linarith have hlen : 2 * hQ < z - a := by dsimp [z, a, d]; linarith have hh : ∀ x ∈ Set.Icc a z, ∃ j : ℤ, |x - (c + (j : ℝ) * Q)| ≤ hQ := by intro x hx rcases hcover x ⟨ha0.trans hx.1, hx.2.trans hz_b⟩ with hxP | hxQ · exfalso apply between_grid_intervals (c := 0) (x := x) (h := hP) hPpos (0 : ℤ) · dsimp [a] at hx norm_num linarith [hx.1] · have heP : e ≤ P - hP := min_le_right _ _ dsimp [z] at hx norm_num linarith [hx.2] · simpa using hxP · exact hxQ exact (not_lt_of_ge (covered_grid_interval_length hQpos hQgap haz hh)) hlen end Math15.LonelyRunner end end /- Proof component: Arithmetic -/ section /-! Elementary arithmetic consequences of the individual acceleration criterion. These results do not assume any unproved classification or prime-gap theorem. -/ namespace Bounty.Arithmetic open Math15.LonelyRunner /-- The half-open gcd window appearing in `ReplacementCondition`. -/ def GcdWindow (n r m : ℕ) : Prop := ∀ b : ℕ, n - r ≤ b → b < m * (n - r) → 1 < Nat.gcd r b theorem replacementCondition_iff (n r w : ℕ) : ReplacementCondition n r w ↔ ∃ m : ℕ, 0 < m ∧ w = m * r ∧ GcdWindow n r m := Iff.rfl theorem replacementCondition_multiplier_ge_two {n r w : ℕ} (hr : r < n) (hw : n ≤ w) (h : ReplacementCondition n r w) : ∃ m : ℕ, 2 ≤ m ∧ w = m * r ∧ GcdWindow n r m := by obtain ⟨m, hm, hmr, hwindow⟩ := h refine ⟨m, ?_, hmr, hwindow⟩ by_contra hn have : m = 1 := by omega simp only [this, one_mul] at hmr omega /-- There is a power of a base greater than one in every interval `[b,p*b)` with positive integral lower endpoint. -/ theorem exists_power_in_mul_interval {p b : ℕ} (hp : 1 < p) (hb : 0 < b) : ∃ e : ℕ, b ≤ p ^ e ∧ p ^ e < p * b := by have hex : ∃ e : ℕ, b ≤ p ^ e := ⟨b, le_of_lt (Nat.lt_pow_self hp)⟩ let e := Nat.find hex have he : b ≤ p ^ e := Nat.find_spec hex refine ⟨e, he, ?_⟩ cases heq : e with | zero => simp only [heq, pow_zero] at he ⊢ nlinarith | succ j => have hj : p ^ j < b := by have hmin := Nat.find_min hex (show j < Nat.find hex by change j < e; omega) omega rw [pow_succ, mul_comm] exact Nat.mul_lt_mul_of_pos_left hj (by omega) /-- A nontrivial valid acceleration cannot have deficit one. -/ theorem gcdWindow_deficit_ge_two {n r m : ℕ} (hr : r < n) (hm : 2 ≤ m) (h : GcdWindow n r m) : 2 ≤ n - r := by by_contra hn have hb : n - r = 1 := by omega have hbad := h 1 (by omega) (by rw [hb, mul_one]; omega) simp at hbad /-- Every prime at most the acceleration multiplier divides the removed speed. -/ theorem gcdWindow_prime_support {n r m p : ℕ} (hr : r < n) (h : GcdWindow n r m) (hp : Nat.Prime p) (hpm : p ≤ m) : p ∣ r := by by_contra hpr obtain ⟨e, helo, hehi⟩ := exists_power_in_mul_interval hp.one_lt (show 0 < n - r by omega) have hbad := h (p ^ e) helo (hehi.trans_le (Nat.mul_le_mul_right (n - r) hpm)) have hcop : Nat.gcd r (p ^ e) = 1 := (hp.coprime_pow_of_not_dvd hpr).gcd_eq_one omega /-- At the midpoint, the next integer is coprime and lies in every nontrivial window. -/ theorem gcdWindow_not_midpoint {n r m : ℕ} (hn : 3 ≤ n) (hr : r < n) (hm : 2 ≤ m) (h : GcdWindow n r m) : n ≠ 2 * r := by intro heq have hr2 : 2 ≤ r := by omega have hb : n - r = r := by omega have hbad := h (r + 1) (by omega) (by rw [hb]; nlinarith) have hcop : Nat.gcd r (r + 1) = 1 := by simp omega /-- The upper-half hypothesis improves to a strict inequality for a valid acceleration. -/ theorem gcdWindow_above_midpoint {n r m : ℕ} (hn : 3 ≤ n) (hr : r < n) (hupper : n - 1 < 2 * r) (hm : 2 ≤ m) (h : GcdWindow n r m) : n < 2 * r := by have hne := gcdWindow_not_midpoint hn hr hm h omega /-- The coprime integer `r-1` gives an explicit upper bound on the valid window. -/ theorem gcdWindow_endpoint_le_pred {n r m : ℕ} (hn : 3 ≤ n) (hr : r < n) (hupper : n - 1 < 2 * r) (hm : 2 ≤ m) (h : GcdWindow n r m) : m * (n - r) ≤ r - 1 := by have hmid := gcdWindow_above_midpoint hn hr hupper hm h have hr1 : 1 ≤ r := by omega by_contra hnot have hbad := h (r - 1) (by omega) (by omega) have hcop : Nat.gcd r (r - 1) = 1 := by exact ((Nat.coprime_self_sub_right hr1).2 (by simp)).gcd_eq_one omega /-- There is a number coprime to a positive `r` above any starting point. -/ theorem exists_coprime_ge (r a : ℕ) (hr : 0 < r) : ∃ x : ℕ, a ≤ x ∧ Nat.Coprime r x := by refine ⟨a * r + 1, ?_, ?_⟩ · nlinarith · simp /-- The first coprime number at or above the deficit. -/ noncomputable def firstCoprime (n r : ℕ) (hr : 0 < r) : ℕ := Nat.find (exists_coprime_ge r (n - r) hr) theorem firstCoprime_spec (n r : ℕ) (hr : 0 < r) : n - r ≤ firstCoprime n r hr ∧ Nat.Coprime r (firstCoprime n r hr) := Nat.find_spec (exists_coprime_ge r (n - r) hr) theorem firstCoprime_le {n r x : ℕ} (hr : 0 < r) (hx : n - r ≤ x) (hcop : Nat.Coprime r x) : firstCoprime n r hr ≤ x := Nat.find_min' (exists_coprime_ge r (n - r) hr) ⟨hx, hcop⟩ /-- A gcd window is valid exactly when its endpoint is no greater than its first coprime number. -/ theorem gcdWindow_iff_endpoint_le_firstCoprime (n r m : ℕ) (hr : 0 < r) : GcdWindow n r m ↔ m * (n - r) ≤ firstCoprime n r hr := by constructor · intro h by_contra hnot obtain ⟨hstart, hcop⟩ := firstCoprime_spec n r hr have hbad := h _ hstart (by omega) rw [hcop.gcd_eq_one] at hbad omega · intro hend x hxstart hxend have hpos := Nat.gcd_pos_of_pos_left x hr by_contra hnot have hcop : Nat.Coprime r x := by show Nat.gcd r x = 1 omega have hmin := firstCoprime_le hr hxstart hcop omega /-- For an upper-half removal, a first coprime occurs before `n`. -/ theorem firstCoprime_lt_n {n r : ℕ} (hn : 3 ≤ n) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) : firstCoprime n r hr < n := by by_cases hmid : n = 2 * r · have hle : firstCoprime n r hr ≤ r + 1 := firstCoprime_le hr (by omega) (by simp) omega · have hle : firstCoprime n r hr ≤ r - 1 := firstCoprime_le hr (by omega) ((Nat.coprime_self_sub_right (show 1 ≤ r by omega)).2 (by simp)) omega /-- A failed upper-half window has a coprime witness below both its endpoint and `n`. -/ theorem not_gcdWindow_witness {n r m : ℕ} (hn : 3 ≤ n) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hbad : ¬ GcdWindow n r m) : ∃ x : ℕ, n - r ≤ x ∧ x < m * (n - r) ∧ x < n ∧ Nat.Coprime r x := by refine ⟨firstCoprime n r hr, (firstCoprime_spec n r hr).1, ?_, firstCoprime_lt_n hn hr hrn hupper, (firstCoprime_spec n r hr).2⟩ have := (gcdWindow_iff_endpoint_le_firstCoprime n r m hr).not.mp hbad omega /-- Prime support implies divisibility by the primorial. -/ theorem gcdWindow_primorial_dvd {n r m : ℕ} (hr : r < n) (h : GcdWindow n r m) : primorial m ∣ r := by exact primorial_dvd_of_prime_support (fun _ hp hpm => gcdWindow_prime_support hr h hp hpm) end Bounty.Arithmetic end /- Proof component: Boundary -/ section namespace Bounty.Boundary open Math15.LonelyRunner /-- A residue representative in the top block of length `r` dominates every congruent positive speed below `n`. -/ theorem representative_dominates {n r x v : ℕ} (hx : n - r ≤ x) (hv : v < n) (hmod : Nat.ModEq r x v) : v ≤ x := by by_contra h have hd : r ∣ v - x := hmod.dvd' have hr := Nat.le_of_dvd (show 0 < v - x by omega) hd omega /-- Cancelling a primitive numerator identifies the binding residue class. -/ theorem binding_speed_le {n r x p v : ℕ} (hx : n - r ≤ x) (hv : v < n) (hp : Nat.Coprime p r) (hpx : Nat.ModEq r (p * x) 1) (hpv : Nat.ModEq r (p * v) 1) : v ≤ x := by apply representative_dominates hx hv exact (hpx.trans hpv.symm).cancel_left_of_coprime hp.symm.gcd_eq_one /-- The exact remainder at the left endpoint of a centered insertion interval. -/ theorem boundary_remainder {c r p v : ℕ} (hc : 0 < c) (hp : 0 < p) (hr : 0 < r) (hv : v < c) (hj : 0 < (v * p) % r) : (v * (c * p - 1)) % (c * r) = c * ((v * p) % r) - v := by let j := (v * p) % r have hjpos : 0 < j := hj have hjr : j < r := Nat.mod_lt _ hr have hvcj : v ≤ c * j := by nlinarith have hjvp : j ≤ v * p := Nat.mod_le _ _ have hvcvp : v ≤ c * (v * p) := by nlinarith have hmod : Nat.ModEq (c * r) (c * (v * p)) (c * j) := (Nat.mod_modEq (v * p) r).symm.mul_left' c have hsub := hmod.sub hvcvp hvcj (Nat.ModEq.refl v) have heq : v * (c * p - 1) = c * (v * p) - v := by have hcp : 1 ≤ c * p := Nat.succ_le_of_lt (Nat.mul_pos hc hp) have hsubcp : c * p - 1 + 1 = c * p := by omega have hsubv : c * (v * p) - v + v = c * (v * p) := by omega nlinarith have hlt : c * j - v < c * r := (Nat.sub_le _ _).trans_lt (Nat.mul_lt_mul_of_pos_left hjr hc) change (v * (c * p - 1)) % (c * r) = c * j - v rw [heq, hsub, Nat.mod_eq_of_lt hlt] /-- Each retained speed is strictly good at the left boundary of an invalid individual acceleration, choosing the primitive center dual to a failed unit. -/ theorem retained_boundary_numerator {n r m p x v : ℕ} (hn : 3 ≤ n) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hm : 2 ≤ m) (hp : 0 < p) (hcop : Nat.Coprime p r) (hpx : Nat.ModEq r (p * x) 1) (hxlo : n - r ≤ x) (hxhi : x < m * (n - r)) (hv : 0 < v) (hvn : v < n) (hvr : v ≠ r) : m * r < min ((v * (n * m * p - 1)) % (n * m * r)) (n * m * r - (v * (n * m * p - 1)) % (n * m * r)) := by have hnot : ¬ r ∣ v := by intro h exact hvr (Nat.eq_of_dvd_of_lt_two_mul (by omega) h (by omega)) have hjpos : 0 < (v * p) % r := by by_contra hh have hdiv : r ∣ v * p := Nat.dvd_of_mod_eq_zero (by omega) exact hnot (hcop.symm.dvd_of_dvd_mul_right hdiv) have hnm : 0 < n * m := by positivity have hvnm : v < n * m := by nlinarith rw [boundary_remainder hnm hp hr hvnm hjpos] let j := (v * p) % r have hj : 0 < j := hjpos have hjr : j < r := Nat.mod_lt _ hr have hleft : m * r < n * m * j - v := by by_cases heq : j = 1 · have hmodeq : Nat.ModEq r (p * v) 1 := by change (p * v) % r = 1 % r have hr1 : 1 < r := by omega change (v * p) % r = 1 at heq simpa only [Nat.mod_eq_of_lt hr1, mul_comm] using heq have hvx := binding_speed_le hxlo hvn hcop hpx hmodeq have hdiff : n - r + r = n := Nat.sub_add_cancel (by omega) have hmul : m * (n - r) + m * r = n * m := by nlinarith change m * r < n * m * j - v rw [heq, mul_one] omega · have hj2 : 2 ≤ j := by omega have hmul := Nat.mul_le_mul_left (n * m) hj2 have hnr : m * r < m * n := Nat.mul_lt_mul_of_pos_left hrn (by omega) rw [mul_comm m n] at hnr omega have hsub : n * m * j - v ≤ n * m * j := Nat.sub_le _ _ have hright : m * r < n * m * r - (n * m * j - v) := by have hgap : j + 1 ≤ r := by omega have hmul := Nat.mul_le_mul_left (n * m) hgap have hnr : m * r < m * n := Nat.mul_lt_mul_of_pos_left hrn (by omega) rw [mul_comm m n] at hnr simp only [Nat.mul_add, Nat.mul_one] at hmul omega exact lt_min hleft hright theorem retained_boundary_distance {n r m p x v : ℕ} (hn : 3 ≤ n) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hm : 2 ≤ m) (hp : 0 < p) (hcop : Nat.Coprime p r) (hpx : Nat.ModEq r (p * x) 1) (hxlo : n - r ≤ x) (hxhi : x < m * (n - r)) (hv : 0 < v) (hvn : v < n) (hvr : v ≠ r) : 1 / (n : ℝ) < distance (v • ((((n * m * p - 1 : ℕ) : ℝ) / (n * m * r : ℕ) : ℝ) : Time)) := by rw [distance_rational_center] have hn0 : (0 : ℝ) < n := by exact_mod_cast (show 0 < n by omega) have hden : (0 : ℝ) < (n * m * r : ℕ) := by positivity apply (div_lt_div_iff₀ hn0 hden).2 have hnum := retained_boundary_numerator hn hr hrn hupper hm hp hcop hpx hxlo hxhi hv hvn hvr have hmul := Nat.mul_lt_mul_of_pos_left hnum (show 0 < n by omega) push_cast norm_num only [one_mul] exact_mod_cast (show n * m * r < min (v * (n * m * p - 1) % (n * m * r)) (n * m * r - v * (n * m * p - 1) % (n * m * r)) * n by nlinarith [hmul]) end Bounty.Boundary end /- Proof component: BoundaryAnalysis -/ section noncomputable section namespace Bounty.Boundary open Math15.LonelyRunner theorem distance_of_integer_sub {A z : ℕ} {t a : ℝ} (heq : (A : ℝ) * t = z - a) (ha : 0 ≤ a) (hhalf : a ≤ 1 / 2) : distance (A • (t : Time)) = a := by have hz : (((z : ℝ) : Time)) = 0 := by apply (AddCircle.coe_eq_zero_iff (1 : ℝ)).2 exact ⟨(z : ℤ), by simp⟩ rw [distance, ← AddCircle.coe_nsmul, nsmul_eq_mul, heq, AddCircle.coe_sub, hz, zero_sub, norm_neg] have hn : ‖(a : Time)‖ = |a| := (AddCircle.norm_coe_eq_abs_iff (1 : ℝ) (by norm_num)).2 (by simpa [abs_of_nonneg ha] using hhalf) simpa [abs_of_nonneg ha] using hn /-- At the left endpoint of one runner's bad interval, another runner must provide the cover whenever the maximum score is bounded by `a`. -/ theorem other_bad_at_left_boundary {U : Finset ℕ} (hU : U.Nonempty) {A z : ℕ} {t a : ℝ} (hA : 0 < A) (ha : 0 < a) (hhalf : a < 1 / 2) (heq : (A : ℝ) * t = z - a) (hML : ML (insert A U) ≤ a) : ∃ v ∈ U, distance (v • (t : Time)) ≤ a := by by_contra hnot push Not at hnot have hscore : a < score U (t : Time) := by simpa only [score, dite_eq_left hU, Finset.lt_inf'_iff] using hnot have hcont : Continuous (fun x : ℝ => score U (x : Time)) := (score_continuous U).comp (AddCircle.continuous_mk' (1 : ℝ)) have hev := continuousAt_const.eventually_lt hcont.continuousAt hscore obtain ⟨δ, hδ, hgood⟩ := Metric.eventually_nhds_iff.mp hev have hAr : (0 : ℝ) < A := by exact_mod_cast hA let e := min (δ / 2) ((1 / 2 - a) / (2 * A)) have he : 0 < e := by dsimp [e]; positivity have heδ : e < δ := (min_le_left _ _).trans_lt (by linarith) have heA : (A : ℝ) * e < 1 / 2 - a := by have hh := min_le_right (δ / 2) ((1 / 2 - a) / (2 * A)) change e ≤ (1 / 2 - a) / (2 * A) at hh have hh' := (le_div_iff₀ (show (0 : ℝ) < 2 * A by positivity)).mp hh nlinarith have hscore' : a < score U ((t - e : ℝ) : Time) := hgood (by rw [Real.dist_eq, sub_sub_cancel_left, abs_neg, abs_of_pos he] exact heδ) have hdistA : a < distance (A • ((t - e : ℝ) : Time)) := by rw [distance_of_integer_sub (z := z) (a := a + A * e) (by nlinarith [heq]) (by positivity) (by linarith)] exact lt_add_of_pos_right _ (mul_pos hAr he) obtain ⟨v, hv, hbad⟩ := geometry_exists_distance_le_of_ML_le (insert A U) (Finset.insert_nonempty _ _) hML ((t - e : ℝ) : Time) rcases Finset.mem_insert.mp hv with rfl | hv · exact (not_lt_of_ge hbad) hdistA · have hh : score U ((t - e : ℝ) : Time) ≤ distance (v • ((t - e : ℝ) : Time)) := by simpa only [score, dite_eq_left hU] using (Finset.inf'_le (fun w => distance (w • ((t - e : ℝ) : Time))) hv) exact (not_lt_of_ge hbad) (hscore'.trans_le hh) end Bounty.Boundary end end /- Proof component: BoundaryConstraint -/ section noncomputable section namespace Bounty.Boundary open Math15.LonelyRunner /-- The other insertion covers the boundary selected by every failed coprime window element. No matching or prime-gap hypothesis is needed for this step. -/ theorem other_insertion_covers_failed_boundary {n r s m p x B : ℕ} (hn : 3 ≤ n) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hm : 2 ≤ m) (hp : 0 < p) (hcop : Nat.Coprime p r) (hpx : Nat.ModEq r (p * x) 1) (hxlo : n - r ≤ x) (hxhi : x < m * (n - r)) (hML : ML (modified n r s (m * r) B) ≤ 1 / (n : ℝ)) : distance (B • ((((n * m * p - 1 : ℕ) : ℝ) / (n * m * r : ℕ) : ℝ) : Time)) ≤ 1 / (n : ℝ) := by let U := (Finset.Icc 1 (n - 1) \ {r, s}) ∪ {B} have hU : U.Nonempty := ⟨B, by simp [U]⟩ have hset : insert (m * r) U = modified n r s (m * r) B := by ext v simp only [U, modified, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] tauto have hn0 : (0 : ℝ) < n := by exact_mod_cast (show 0 < n by omega) have hm0 : (0 : ℝ) < m := by exact_mod_cast (show 0 < m by omega) have hr0 : (0 : ℝ) < r := by exact_mod_cast hr have hlarge : 1 ≤ n * m * p := Nat.succ_le_of_lt (by positivity) have hphase : (m * r : ℕ) * (((n * m * p - 1 : ℕ) : ℝ) / (n * m * r : ℕ)) = (m * p : ℕ) - 1 / (n : ℝ) := by simp only [Nat.cast_sub hlarge, Nat.cast_one, Nat.cast_mul] field_simp obtain ⟨v, hv, hbad⟩ := other_bad_at_left_boundary hU (show 0 < m * r by positivity) (show (0 : ℝ) < 1 / n by positivity) (show 1 / (n : ℝ) < 1 / 2 by exact one_div_lt_one_div_of_lt (by norm_num) (by exact_mod_cast hn)) hphase (by simpa [hset] using hML) simp only [U, Finset.mem_union, Finset.mem_sdiff, Finset.mem_Icc, Finset.mem_insert, Finset.mem_singleton] at hv rcases hv with ⟨⟨hvpos, hvn⟩, hvr⟩ | rfl · have hgood := retained_boundary_distance hn hr hrn hupper hm hp hcop hpx hxlo hxhi (show 0 < v by omega) (show v < n by omega) (show v ≠ r by intro heq; exact hvr (Or.inl heq)) exact False.elim ((not_lt_of_ge hbad) hgood) · exact hbad /-- An entirely natural-number necessary condition, suitable for certified finite boundary tests. -/ theorem integer_boundary_condition {n r s m p x B : ℕ} (hn : 3 ≤ n) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hm : 2 ≤ m) (hp : 0 < p) (hcop : Nat.Coprime p r) (hpx : Nat.ModEq r (p * x) 1) (hxlo : n - r ≤ x) (hxhi : x < m * (n - r)) (hML : ML (modified n r s (m * r) B) ≤ 1 / (n : ℝ)) : min ((B * (n * m * p - 1)) % (n * m * r)) (n * m * r - (B * (n * m * p - 1)) % (n * m * r)) ≤ m * r := by have hd := other_insertion_covers_failed_boundary hn hr hrn hupper hm hp hcop hpx hxlo hxhi hML rw [distance_rational_center] at hd have hn0 : (0 : ℝ) < n := by exact_mod_cast (show 0 < n by omega) have hden : (0 : ℝ) < (n * m * r : ℕ) := by positivity have hcross := (div_le_div_iff₀ hden hn0).mp hd norm_num only [one_mul] at hcross have hnat : min ((B * (n * m * p - 1)) % (n * m * r)) (n * m * r - (B * (n * m * p - 1)) % (n * m * r)) * n ≤ n * m * r := by exact_mod_cast hcross have hnat' : n * min ((B * (n * m * p - 1)) % (n * m * r)) (n * m * r - (B * (n * m * p - 1)) % (n * m * r)) ≤ n * (m * r) := by nlinarith [hnat] exact Nat.le_of_mul_le_mul_left hnat' (by omega) /-- A rejected boundary test disproves tightness in the original analytic definition, without trusting an external numerical computation. -/ theorem boundary_obstruction {n r s m p x B : ℕ} (hn : 3 ≤ n) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hm : 2 ≤ m) (hp : 0 < p) (hcop : Nat.Coprime p r) (hpx : Nat.ModEq r (p * x) 1) (hxlo : n - r ≤ x) (hxhi : x < m * (n - r)) (hbad : m * r < min ((B * (n * m * p - 1)) % (n * m * r)) (n * m * r - (B * (n * m * p - 1)) % (n * m * r))) : 1 / (n : ℝ) < ML (modified n r s (m * r) B) := by apply lt_of_not_ge intro hML exact (not_lt_of_ge (integer_boundary_condition hn hr hrn hupper hm hp hcop hpx hxlo hxhi hML)) hbad end Bounty.Boundary end end /- Proof component: BoundaryResidue -/ section noncomputable section namespace Bounty.Boundary open Math15.LonelyRunner /-- A covered failed boundary has an integral displacement satisfying both the congruence and the narrow absolute-value constraint. -/ theorem boundary_residue_exists {n r s m p x B : ℕ} (hn : 3 ≤ n) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hm : 2 ≤ m) (hp : 0 < p) (hcop : Nat.Coprime p r) (hpx : Nat.ModEq r (p * x) 1) (hxlo : n - r ≤ x) (hxhi : x < m * (n - r)) (hML : ML (modified n r s (m * r) B) ≤ 1 / (n : ℝ)) : ∃ D : ℤ, (r : ℤ) ∣ D * x - B ∧ |(n : ℤ) * m * D - B| ≤ (m : ℤ) * r := by have hbad := other_insertion_covers_failed_boundary hn hr hrn hupper hm hp hcop hpx hxlo hxhi hML rw [distance, ← AddCircle.coe_nsmul, nsmul_eq_mul, AddCircle.norm_eq] at hbad simp only [inv_one, one_mul, mul_one] at hbad let t : ℝ := ((n * m * p - 1 : ℕ) : ℝ) / (n * m * r : ℕ) let z : ℤ := round ((B : ℝ) * t) let D : ℤ := (B : ℤ) * p - z * r change |(B : ℝ) * t - z| ≤ 1 / (n : ℝ) at hbad have hn0 : (0 : ℝ) < n := by exact_mod_cast (show 0 < n by omega) have hm0 : (0 : ℝ) < m := by exact_mod_cast (show 0 < m by omega) have hr0 : (0 : ℝ) < r := by exact_mod_cast hr have hden : (0 : ℝ) < (n * m * r : ℕ) := by positivity have hlarge : 1 ≤ n * m * p := Nat.succ_le_of_lt (by positivity) have heq : ((B : ℝ) * t - z) * (n * m * r : ℕ) = (n : ℝ) * m * (D : ℝ) - B := by dsimp [t, D] push_cast rw [Nat.cast_sub hlarge, Nat.cast_one] push_cast field_simp <;> ring have hbound : |(n : ℝ) * m * (D : ℝ) - B| ≤ (m : ℝ) * r := by calc |(n : ℝ) * m * (D : ℝ) - B| = |((B : ℝ) * t - z) * (n * m * r : ℕ)| := by rw [heq] _ = |(B : ℝ) * t - z| * (n * m * r : ℕ) := by rw [abs_mul, abs_of_pos hden] _ ≤ (1 / (n : ℝ)) * (n * m * r : ℕ) := mul_le_mul_of_nonneg_right hbad hden.le _ = (m : ℝ) * r := by push_cast; field_simp refine ⟨D, ?_, by exact_mod_cast hbound⟩ have hdiv : (r : ℤ) ∣ (p : ℤ) * x - 1 := by simpa only [Nat.cast_one, Nat.cast_mul, neg_sub] using dvd_neg.mpr hpx.dvd have hdiv1 := dvd_mul_of_dvd_right hdiv (B : ℤ) have hdiv2 : (r : ℤ) ∣ z * r * x := by refine ⟨z * x, ?_⟩ ring convert dvd_sub hdiv1 hdiv2 using 1 <;> dsimp [D] <;> ring /-- The faster insertion makes the displacement strictly positive. -/ theorem positive_boundary_residue {n r s m p x B : ℕ} (hn : 3 ≤ n) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hm : 2 ≤ m) (hp : 0 < p) (hcop : Nat.Coprime p r) (hpx : Nat.ModEq r (p * x) 1) (hxlo : n - r ≤ x) (hxhi : x < m * (n - r)) (hfast : m * r < B) (hML : ML (modified n r s (m * r) B) ≤ 1 / (n : ℝ)) : ∃ D : ℕ, 0 < D ∧ Nat.ModEq r (D * x) B ∧ |(n : ℤ) * m * D - B| ≤ (m : ℤ) * r := by obtain ⟨D, hdiv, hb⟩ := boundary_residue_exists hn hr hrn hupper hm hp hcop hpx hxlo hxhi hML have hfast' : (m : ℤ) * r < B := by exact_mod_cast hfast have hD : 0 < D := by by_contra hnot have hmul : (n : ℤ) * m * D ≤ 0 := mul_nonpos_of_nonneg_of_nonpos (by positivity) (le_of_not_gt hnot) have hlo := (abs_le.mp hb).1 linarith have hcast : (D.toNat : ℤ) = D := Int.toNat_of_nonneg hD.le refine ⟨D.toNat, by omega, ?_, by simpa only [hcast] using hb⟩ apply Nat.modEq_iff_dvd.mpr simpa only [Nat.cast_mul, hcast, neg_sub] using dvd_neg.mpr hdiv /-- A unit cannot remove a common factor of the insertion and removal. -/ theorem boundary_residue_gcd_dvd {r x B D : ℕ} (hx : Nat.Coprime x r) (hmod : Nat.ModEq r (D * x) B) : Nat.gcd B r ∣ D := by have hdx : Nat.gcd B r ∣ D * x := (hmod.dvd_iff (Nat.gcd_dvd_right B r)).2 (Nat.gcd_dvd_left B r) have hcop : Nat.Coprime (Nat.gcd B r) x := hx.symm.of_dvd_left (Nat.gcd_dvd_right B r) exact hcop.dvd_mul_right.mp hdx /-- The narrow displacement interval contains at most one multiple of a common divisor at least two. -/ theorem boundary_residue_unique {n r m B d D E : ℕ} (hrn : r < n) (hm : 0 < m) (hd : 2 ≤ d) (hdD : d ∣ D) (hdE : d ∣ E) (hD : |(n : ℤ) * m * D - B| ≤ (m : ℤ) * r) (hE : |(n : ℤ) * m * E - B| ≤ (m : ℤ) * r) : D = E := by suffices hle : ∀ A C : ℕ, d ∣ A → d ∣ C → |(n : ℤ) * m * A - B| ≤ (m : ℤ) * r → |(n : ℤ) * m * C - B| ≤ (m : ℤ) * r → A ≤ C → A = C by rcases le_total D E with h | h · exact hle D E hdD hdE hD hE h · exact (hle E D hdE hdD hE hD h).symm intro A C hdA hdC hA hC hAC by_contra hne have hdiffpos : 0 < C - A := by omega have hdiff : d ∣ C - A := Nat.dvd_sub hdC hdA have hdiffle : d ≤ C - A := Nat.le_of_dvd hdiffpos hdiff have hgap : (A : ℤ) + 2 ≤ C := by omega have hmul := mul_le_mul_of_nonneg_left hgap (show (0 : ℤ) ≤ (n : ℤ) * m by positivity) have hnmr : (m : ℤ) * r < (m : ℤ) * n := mul_lt_mul_of_pos_left (by exact_mod_cast hrn) (by exact_mod_cast hm) have hAlo := (abs_le.mp hA).1 have hChi := (abs_le.mp hC).2 nlinarith end Bounty.Boundary end end /- Proof component: Fastest -/ section noncomputable section namespace Bounty open Math15.LonelyRunner Arithmetic Boundary theorem primitive_inverse_exists {r x : ℕ} (hr : 1 < r) (hx : Nat.Coprime x r) : ∃ p : ℕ, 0 < p ∧ Nat.Coprime p r ∧ Nat.ModEq r (p * x) 1 := by letI : NeZero r := ⟨by omega⟩ let p := ((x : ZMod r)⁻¹).val have hmod : Nat.ModEq r (p * x) 1 := by apply (ZMod.natCast_eq_natCast_iff (p * x) 1 r).mp simpa only [Nat.cast_mul, Nat.cast_one] using ZMod.val_inv_mul hx have hcop : Nat.Coprime p r := Nat.coprime_of_mul_modEq_one x hmod refine ⟨p, ?_, hcop, hmod⟩ by_contra hnot have hp : p = 0 := by omega have : r = 1 := by simpa only [hp, Nat.coprime_zero_left] using hcop omega theorem narrow_slower_residue {C H B D : ℤ} (hC : H < C) (hH : 0 ≤ H) (hB : 0 ≤ B) (hBH : B < H) (hbound : |C * D - B| ≤ H) : D = 0 ∨ D = 1 := by have hlo := (abs_le.mp hbound).1 have hhi := (abs_le.mp hbound).2 have hnonneg : 0 ≤ D := by by_contra hnot have hD : D ≤ -1 := by omega have hmul := mul_le_mul_of_nonneg_left hD (show 0 ≤ C by omega) nlinarith have hle : D ≤ 1 := by by_contra hnot have hD : 2 ≤ D := by omega have hmul := mul_le_mul_of_nonneg_left hD (show 0 ≤ C by omega) nlinarith omega /-- A faster exclusive insertion obeys the individual gcd-window condition whenever it shares a nontrivial gcd with the slower insertion's modulus. -/ theorem fastest_exclusive_window {n r s m B : ℕ} (hn : 3 ≤ n) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hm : 2 ≤ m) (hfast : B < m * r) (hexclusive : ¬ r ∣ B) (hgcd : 2 ≤ Nat.gcd B r) (hML : ML (modified n r s (m * r) B) ≤ 1 / (n : ℝ)) : GcdWindow n r m := by by_contra hnot obtain ⟨x, hxlo, hxhi, _, hxr⟩ := not_gcdWindow_witness hn hr hrn hupper hnot obtain ⟨p, hp, hcop, hpx⟩ := primitive_inverse_exists (show 1 < r by omega) hxr.symm obtain ⟨D, hdiv, hbound⟩ := boundary_residue_exists hn hr hrn hupper hm hp hcop hpx hxlo hxhi hML have hmrnm : (m : ℤ) * r < (n : ℤ) * m := by have h := Nat.mul_lt_mul_of_pos_left hrn (show 0 < m by omega) exact_mod_cast (by nlinarith [h] : m * r < n * m) have hfast' : (B : ℤ) < (m : ℤ) * r := by exact_mod_cast hfast rcases narrow_slower_residue hmrnm (by positivity) (by positivity) hfast' hbound with hD | hD · subst D have hdivB : (r : ℤ) ∣ (B : ℤ) := by simpa using hdiv exact hexclusive (Int.natCast_dvd_natCast.mp hdivB) · subst D have hmod : Nat.ModEq r x B := by apply Nat.modEq_iff_dvd.mpr simpa only [one_mul, neg_sub] using dvd_neg.mpr hdiv have hgcd' : Nat.gcd B r = 1 := by rw [← hmod.gcd_eq] exact hxr.symm.gcd_eq_one omega end Bounty end end /- Proof component: CommonResidue -/ section noncomputable section namespace Bounty open Math15.LonelyRunner Arithmetic Boundary theorem gcd_boundary_residue {r x B D : ℕ} (hx : Nat.Coprime x r) (hmod : Nat.ModEq r (D * x) B) : Nat.gcd D r = Nat.gcd B r := by apply Nat.dvd_antisymm · rw [← hmod.gcd_eq] exact Nat.dvd_gcd (dvd_mul_of_dvd_left (Nat.gcd_dvd_left D r) x) (Nat.gcd_dvd_right D r) · exact Nat.dvd_gcd (boundary_residue_gcd_dvd hx hmod) (Nat.gcd_dvd_right B r) /-- All failed coprime flanks have one common displacement, because the permitted interval has width below two and the common divisor is at least two. -/ theorem failed_window_common_residue {n r s m B : ℕ} (hn : 3 ≤ n) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hm : 2 ≤ m) (hfast : m * r < B) (hgcd : 2 ≤ Nat.gcd B r) (hML : ML (modified n r s (m * r) B) ≤ 1 / (n : ℝ)) (hbad : ¬ GcdWindow n r m) : ∃ D : ℕ, 0 < D ∧ 2 ≤ D ∧ Nat.gcd D r = Nat.gcd B r ∧ |(n : ℤ) * m * D - B| ≤ (m : ℤ) * r ∧ ∀ x : ℕ, n - r ≤ x → x < m * (n - r) → Nat.Coprime x r → Nat.ModEq r (D * x) B := by obtain ⟨x, hxlo, hxhi, _, hx⟩ := not_gcdWindow_witness hn hr hrn hupper hbad obtain ⟨p, hp, hpcop, hpx⟩ := primitive_inverse_exists (show 1 < r by omega) hx.symm obtain ⟨D, hDpos, hmod, hbound⟩ := positive_boundary_residue hn hr hrn hupper hm hp hpcop hpx hxlo hxhi hfast hML have hdivD := boundary_residue_gcd_dvd hx.symm hmod have hDtwo : 2 ≤ D := hgcd.trans (Nat.le_of_dvd hDpos hdivD) refine ⟨D, hDpos, hDtwo, gcd_boundary_residue hx.symm hmod, hbound, ?_⟩ intro y hylo hyhi hy obtain ⟨q, hq, hqcop, hqy⟩ := primitive_inverse_exists (show 1 < r by omega) hy obtain ⟨E, _, hmodE, hboundE⟩ := positive_boundary_residue hn hr hrn hupper hm hq hqcop hqy hylo hyhi hfast hML have hdivE := boundary_residue_gcd_dvd hy hmodE have heq : D = E := boundary_residue_unique hrn (by omega) hgcd hdivD hdivE hbound hboundE exact heq ▸ hmodE /-- The narrow displacement bound forces the multiplier of an invalid slower replacement to be strictly smaller than the faster multiplier. -/ theorem residue_multiplier_bound {n r s m k D : ℕ} (hrn : r < n) (hsn : s < n) (hm : 0 < m) (hk : 0 < k) (hbound : |(n : ℤ) * m * D - (k : ℤ) * s| ≤ (m : ℤ) * r) : m * D < m + k := by have hn0 : (0 : ℤ) < n := by exact_mod_cast (show 0 < n by omega) have hmr : (m : ℤ) * r < (m : ℤ) * n := mul_lt_mul_of_pos_left (by exact_mod_cast hrn) (by exact_mod_cast hm) have hks : (k : ℤ) * s < (k : ℤ) * n := mul_lt_mul_of_pos_left (by exact_mod_cast hsn) (by exact_mod_cast hk) have hh := (abs_le.mp hbound).2 have hprod : ((m : ℤ) * D) * n < ((m : ℤ) + k) * n := by nlinarith have hfinal := (mul_lt_mul_iff_left₀ hn0).mp hprod exact_mod_cast hfinal theorem slower_multiplier_lt_faster {n r s m k D : ℕ} (hrn : r < n) (hsn : s < n) (hm : 2 ≤ m) (hk : 0 < k) (hD : 2 ≤ D) (hbound : |(n : ℤ) * m * D - (k : ℤ) * s| ≤ (m : ℤ) * r) : m < k ∧ 3 ≤ k := by have h := residue_multiplier_bound hrn hsn (show 0 < m by omega) hk hbound have hmul := Nat.mul_le_mul_left m hD constructor <;> omega end Bounty end end /- Proof component: CoprimeGaps -/ section namespace Bounty.CoprimeGaps /-- An explicit gap bound; proving this for `J = 2^ω(r)` is a separate number-theoretic obligation. -/ def HasCoprimeGaps (r J : ℕ) : Prop := ∀ a : ℕ, ∃ x : ℕ, a ≤ x ∧ x < a + J ∧ Nat.Coprime x r theorem unit_spacing {r D B x y : ℕ} (hr : 0 < r) (hx : Nat.ModEq r (D * x) B) (hy : Nat.ModEq r (D * y) B) (hxy : x < y) : r / Nat.gcd r D ≤ y - x := by have hmod := (hx.trans hy.symm).cancel_left_div_gcd hr exact Nat.le_of_dvd (Nat.sub_pos_of_lt hxy) hmod.dvd' /-- A common residue cannot persist on two units in an interval when its period exceeds a bound on consecutive coprime gaps. -/ theorem at_most_one_unit {r J D B a b : ℕ} (hr : 0 < r) (hgap : HasCoprimeGaps r J) (hperiod : J < r / Nat.gcd r D) (hcong : ∀ x : ℕ, a ≤ x → x < b → Nat.Coprime x r → Nat.ModEq r (D * x) B) : ∀ x y : ℕ, a ≤ x → x < b → Nat.Coprime x r → a ≤ y → y < b → Nat.Coprime y r → x = y := by have hclose : ∀ x y : ℕ, a ≤ x → x < b → Nat.Coprime x r → a ≤ y → y < b → Nat.Coprime y r → x < y → y ≤ x + J → False := by intro x y hxlo hxhi hx hylo hyhi hy hxy hdist have hspace := unit_spacing hr (hcong x hxlo hxhi hx) (hcong y hylo hyhi hy) hxy omega have hinc : ∀ x y : ℕ, a ≤ x → x < b → Nat.Coprime x r → a ≤ y → y < b → Nat.Coprime y r → x < y → False := by intro x y hxlo hxhi hx hylo hyhi hy hxy by_cases hnear : y ≤ x + J · exact hclose x y hxlo hxhi hx hylo hyhi hy hxy hnear · obtain ⟨z, hzlo, hzhi, hz⟩ := hgap (x + 1) exact hclose x z hxlo hxhi hx (by omega) (by omega) hz (by omega) (by omega) intro x y hxlo hxhi hx hylo hyhi hy rcases lt_trichotomy x y with hxy | hxy | hxy · exact False.elim (hinc x y hxlo hxhi hx hylo hyhi hy hxy) · exact hxy · exact False.elim (hinc y x hylo hyhi hy hxlo hxhi hx hxy) theorem unique_window_start_lt_two_gaps {r J a m : ℕ} (hgap : HasCoprimeGaps r J) (hm : 2 ≤ m) (hunique : ∀ x y : ℕ, a ≤ x → x < m * a → Nat.Coprime x r → a ≤ y → y < m * a → Nat.Coprime y r → x = y) : a < 2 * J := by by_contra hnot obtain ⟨x, hxlo, hxhi, hx⟩ := hgap a obtain ⟨y, hylo, hyhi, hy⟩ := hgap (a + J) have hmul : 2 * a ≤ m * a := Nat.mul_le_mul_right a hm have hxy := hunique x y hxlo (by omega) hx (by omega) (by omega) hy omega theorem small_window_of_separation {r J a m k : ℕ} (ha : a < 2 * J) (hmk : m < k) (hsep : 8 * k * J < r) : 4 * (m * a) < r := by have hmul1 : m * a ≤ m * (2 * J) := Nat.mul_le_mul_left m ha.le have hmul2 : m * (2 * J) ≤ k * (2 * J) := Nat.mul_le_mul_right (2 * J) hmk.le nlinarith end Bounty.CoprimeGaps end /- Proof component: MixedCase -/ section namespace Bounty.MixedCase /-- The purely integral uniqueness argument in the doubling/tripling reduction. The assumptions name each input needed from the number theoretic reduction; no prime-gap or covering theorem is assumed implicitly. -/ theorem unique_reduced_multipliers {G m k L D : ℕ} (hG : 2 ≤ G) (hm : 2 ≤ m) (hmk : m < k) (hGL : G < L) (hLmG : L < m * G) (hLk : L ≤ k) (hproduct : D * L = k * G) (hGD : G ≤ D) (hD : m * D < m + k) (hunique : ∀ j : ℕ, G < j → j ≤ k → j ≤ m * G → Nat.Coprime j G → j = L) : G = 2 ∧ m = 2 ∧ k = 3 ∧ L = 3 ∧ D = 2 := by have hG1 : 1 ≤ G := by omega have hmkG : m * G < m + k := lt_of_le_of_lt (Nat.mul_le_mul_left m hGD) hD have hpred : m * (G - 1) + m = m * G := by simpa [Nat.mul_add] using congrArg (fun t => m * t) (Nat.sub_add_cancel hG1) have hGtwo : G = 2 := by by_contra hnot have hG3 : 3 ≤ G := by omega have hk : 2 * G - 1 ≤ k := by have hmono := Nat.mul_le_mul_right (G - 1) hm omega have hGplus : G + 1 ≤ k := by omega have hcop1 : Nat.Coprime (G + 1) G := by simp have hcop2 : Nat.Coprime (2 * G - 1) G := by have heq : 2 * G - 1 = (G - 1) + G := by omega rw [heq, Nat.coprime_add_self_left] exact (Nat.coprime_self_sub_left hG1).2 (by simp) have hfirst := hunique (G + 1) (by omega) hGplus (by nlinarith) hcop1 have hsecond := hunique (2 * G - 1) (by omega) hk (by nlinarith) hcop2 omega subst G have hmtwo : m = 2 := by by_contra hnot have hm3 : 3 ≤ m := by omega by_cases hk5 : 5 ≤ k · have hfirst := hunique 3 (by omega) (by omega) (by omega) (by decide) have hsecond := hunique 5 (by omega) hk5 (by omega) (by decide) omega · have hmthree : m = 3 := by omega have hkfour : k = 4 := by omega have hLthree := hunique 3 (by omega) (by omega) (by omega) (by decide) rw [← hLthree, hkfour] at hproduct omega subst m have hLthree : L = 3 := by omega subst L have hklt : k < 6 := by omega have hkthree : k = 3 := by omega subst k have hDtwo : D = 2 := by omega exact ⟨rfl, rfl, rfl, rfl, hDtwo⟩ /-- Coprime multipliers in the short auxiliary interval provide distinct coprime numbers in the original failed window. -/ theorem scaled_unit_uniqueness {G h b m k L r : ℕ} (hb : 0 < b) (hm : 0 < m) (hbh : b ≤ h) (hhcop : Nat.Coprime h r) (htransfer : ∀ j : ℕ, j ≤ k → Nat.Coprime j G → Nat.Coprime j r) (hunique : ∀ x : ℕ, G * h + b ≤ x → x < m * (G * h + b) → Nat.Coprime x r → x = L * h) : ∀ j : ℕ, G < j → j ≤ k → j ≤ m * G → Nat.Coprime j G → j = L := by intro j hjG hjk hjm hjcop have hh : 0 < h := by omega have hlo : G * h + b ≤ j * h := by have hj : G + 1 ≤ j := by omega have hmul := Nat.mul_le_mul_right h hj nlinarith have hhi : j * h < m * (G * h + b) := by have hmul := Nat.mul_le_mul_right h hjm nlinarith have heq := hunique (j * h) hlo hhi ((htransfer j hjk hjcop).mul_left hhcop) exact Nat.mul_right_cancel hh heq /-- The failed-window and support inputs give the precise integral hypotheses of `unique_reduced_multipliers`. Valuation decomposition is represented by `hproduct`, `hGD`, `hLk`, and `hLcop`. -/ theorem interval_unique_reduction {G h b m k L D r s : ℕ} (hG : 2 ≤ G) (hm : 2 ≤ m) (hmk : m < k) (hb : 0 < b) (hLk : L ≤ k) (hLcop : Nat.Coprime L G) (hproduct : D * L = k * G) (hGD : G ≤ D) (hD : m * D < m + k) (hlo : G * h + b ≤ L * h) (hhi : L * h < m * (G * h + b)) (hflank : k * b ≤ L * h) (hhcopr : Nat.Coprime h r) (hhcops : Nat.Coprime h s) (hwindow : ∀ y : ℕ, b ≤ y → y < k * b → ¬ Nat.Coprime y s) (htransfer : ∀ j : ℕ, j ≤ k → Nat.Coprime j G → Nat.Coprime j r) (hunique : ∀ x : ℕ, G * h + b ≤ x → x < m * (G * h + b) → Nat.Coprime x r → x = L * h) : G = 2 ∧ m = 2 ∧ k = 3 ∧ L = 3 ∧ D = 2 ∧ 3 * b ≤ h := by have hkh : k * b ≤ k * h := hflank.trans (Nat.mul_le_mul_right h hLk) have hbh : b ≤ h := Nat.le_of_mul_le_mul_left hkh (by omega) have hkb : k * b ≤ h := by by_contra hnot exact hwindow h hbh (by omega) hhcops have hGL : G < L := by by_contra hnot have hmul := Nat.mul_le_mul_right h (show L ≤ G by omega) omega have hmbh : m * b < h := by have hmul := Nat.mul_lt_mul_of_pos_right hmk hb omega have hLmG : L < m * G := by have hle : L ≤ m * G := by by_contra hnot have hmul := Nat.mul_le_mul_right h (show m * G + 1 ≤ L by omega) nlinarith by_contra hnot have heq : L = m * G := by omega have hdiv : G ∣ L := by rw [heq]; exact Nat.dvd_mul_left G m have : G = 1 := hLcop.symm.eq_one_of_dvd hdiv omega obtain ⟨hG2, hm2, hk3, hL3, hD2⟩ := unique_reduced_multipliers hG hm hmk hGL hLmG hLk hproduct hGD hD (scaled_unit_uniqueness hb (by omega) hbh hhcopr htransfer hunique) exact ⟨hG2, hm2, hk3, hL3, hD2, by simpa [hk3] using hkb⟩ end Bounty.MixedCase end /- Proof component: SmoothPair -/ section namespace Bounty.SmoothPair /-- Two geometric progressions with alternating ratios below two hit every doubling interval beyond their first element. -/ theorem hits_doubling_interval {p q a : ℕ} (hp : 0 < p) (hpa : p ≤ a) (hpq : 3 * p < 2 * q) (hqp : q < 2 * p) : ∃ z : ℕ, a ≤ z ∧ z < 2 * a ∧ ((∃ e : ℕ, z = p * 3 ^ e) ∨ (∃ e : ℕ, z = q * 3 ^ e)) := by have ha : 0 < a := by omega have hex : ∃ e : ℕ, a ≤ p * 3 ^ e := by refine ⟨a, ?_⟩ have hpow : a < 3 ^ a := Nat.lt_pow_self (by norm_num) have hmul : 3 ^ a ≤ p * 3 ^ a := by nlinarith omega let e := Nat.find hex have he : a ≤ p * 3 ^ e := Nat.find_spec hex by_cases hsmall : p * 3 ^ e < 2 * a · exact ⟨p * 3 ^ e, he, hsmall, Or.inl ⟨e, rfl⟩⟩ have he0 : e ≠ 0 := by intro hzero simp only [hzero, pow_zero, mul_one] at hsmall omega obtain ⟨j, hj⟩ := Nat.exists_eq_succ_of_ne_zero he0 have hprev : p * 3 ^ j < a := by have hmin := Nat.find_min hex (show j < Nat.find hex by change j < e; omega) omega have hpowpos : 0 < 3 ^ j := by positivity have hlow := Nat.mul_lt_mul_of_pos_right hpq hpowpos have hhigh := Nat.mul_lt_mul_of_pos_right hqp hpowpos rw [hj, pow_succ] at hsmall refine ⟨q * 3 ^ j, ?_, ?_, Or.inr ⟨j, rfl⟩⟩ · nlinarith · nlinarith /-- The unique-unit conclusion is incompatible with a pair of smooth bases and a nontrivial divisor of the proposed unique unit coprime to both bases. -/ theorem unique_unit_impossible {r a p q x h : ℕ} (hp : 0 < p) (hpa : p ≤ a) (hpq : 3 * p < 2 * q) (hqp : q < 2 * p) (hpr : Nat.Coprime p r) (hqr : Nat.Coprime q r) (h3r : Nat.Coprime 3 r) (hh : 1 < h) (hhx : h ∣ x) (hhp : Nat.Coprime h p) (hhq : Nat.Coprime h q) (hh3 : Nat.Coprime h 3) (hunique : ∀ z : ℕ, a ≤ z → z < 2 * a → Nat.Coprime z r → z = x) : False := by obtain ⟨z, hzlo, hzhi, hform⟩ := hits_doubling_interval hp hpa hpq hqp have hzr : Nat.Coprime z r := by rcases hform with ⟨e, rfl⟩ | ⟨e, rfl⟩ · exact hpr.mul_left (h3r.pow_left e) · exact hqr.mul_left (h3r.pow_left e) have hhz : Nat.Coprime h z := by rcases hform with ⟨e, rfl⟩ | ⟨e, rfl⟩ · exact hhp.mul_right (hh3.pow_right e) · exact hhq.mul_right (hh3.pow_right e) have heq : z = x := hunique z hzlo hzhi hzr have hhone : h = 1 := hhz.eq_one_of_dvd (heq ▸ hhx) omega end Bounty.SmoothPair end /- Proof component: FiniteArithmetic -/ section namespace Bounty.FiniteArithmetic /-- A short explicit prime certificate bounds the deficit below 20000. The proof needs no Jacobsthal or prime-interval theorem. -/ theorem deficit_le_four {s b : ℕ} (hs : 0 < s) (hsbound : s < 20000) (hbs : b < s) (hnbound : s + b ≤ 20000) (h2 : 2 ∣ s) (h3 : 3 ∣ s) (hprime : ∀ p : ℕ, Nat.Prime p → b ≤ p → p < 3 * b → p ∣ s) : b ≤ 4 := by by_contra hnot have h6 : 6 ∣ s := (by norm_num : Nat.Coprime 2 3).mul_dvd_of_dvd_of_dvd h2 h3 by_cases hb0 : b ≤ 5 · have hp5 : 5 ∣ s := hprime 5 (by norm_num) (by omega) (by omega) have hp7 : 7 ∣ s := hprime 7 (by norm_num) (by omega) (by omega) have hp11 : 11 ∣ s := hprime 11 (by norm_num) (by omega) (by omega) have hp13 : 13 ∣ s := hprime 13 (by norm_num) (by omega) (by omega) have hd30 : 30 ∣ s := (by norm_num : Nat.Coprime 6 5).mul_dvd_of_dvd_of_dvd h6 hp5 have hd210 : 210 ∣ s := (by norm_num : Nat.Coprime 30 7).mul_dvd_of_dvd_of_dvd hd30 hp7 have hd2310 : 2310 ∣ s := (by norm_num : Nat.Coprime 210 11).mul_dvd_of_dvd_of_dvd hd210 hp11 have hd30030 : 30030 ∣ s := (by norm_num : Nat.Coprime 2310 13).mul_dvd_of_dvd_of_dvd hd2310 hp13 have hle := Nat.le_of_dvd hs hd30030 exact (not_le_of_gt hsbound) ((show 20000 ≤ 30030 by decide).trans hle) by_cases hb1 : b ≤ 6 · have hp7 : 7 ∣ s := hprime 7 (by norm_num) (by omega) (by omega) have hp11 : 11 ∣ s := hprime 11 (by norm_num) (by omega) (by omega) have hp13 : 13 ∣ s := hprime 13 (by norm_num) (by omega) (by omega) have hp17 : 17 ∣ s := hprime 17 (by norm_num) (by omega) (by omega) have hd42 : 42 ∣ s := (by norm_num : Nat.Coprime 6 7).mul_dvd_of_dvd_of_dvd h6 hp7 have hd462 : 462 ∣ s := (by norm_num : Nat.Coprime 42 11).mul_dvd_of_dvd_of_dvd hd42 hp11 have hd6006 : 6006 ∣ s := (by norm_num : Nat.Coprime 462 13).mul_dvd_of_dvd_of_dvd hd462 hp13 have hd102102 : 102102 ∣ s := (by norm_num : Nat.Coprime 6006 17).mul_dvd_of_dvd_of_dvd hd6006 hp17 have hle := Nat.le_of_dvd hs hd102102 exact (not_le_of_gt hsbound) ((show 20000 ≤ 102102 by decide).trans hle) by_cases hb2 : b ≤ 13 · have hp13 : 13 ∣ s := hprime 13 (by norm_num) (by omega) (by omega) have hp17 : 17 ∣ s := hprime 17 (by norm_num) (by omega) (by omega) have hp19 : 19 ∣ s := hprime 19 (by norm_num) (by omega) (by omega) have hd78 : 78 ∣ s := (by norm_num : Nat.Coprime 6 13).mul_dvd_of_dvd_of_dvd h6 hp13 have hd1326 : 1326 ∣ s := (by norm_num : Nat.Coprime 78 17).mul_dvd_of_dvd_of_dvd hd78 hp17 have hd25194 : 25194 ∣ s := (by norm_num : Nat.Coprime 1326 19).mul_dvd_of_dvd_of_dvd hd1326 hp19 have hle := Nat.le_of_dvd hs hd25194 exact (not_le_of_gt hsbound) ((show 20000 ≤ 25194 by decide).trans hle) by_cases hb3 : b ≤ 31 · have hp31 : 31 ∣ s := hprime 31 (by norm_num) (by omega) (by omega) have hp37 : 37 ∣ s := hprime 37 (by norm_num) (by omega) (by omega) have hp41 : 41 ∣ s := hprime 41 (by norm_num) (by omega) (by omega) have hd186 : 186 ∣ s := (by norm_num : Nat.Coprime 6 31).mul_dvd_of_dvd_of_dvd h6 hp31 have hd6882 : 6882 ∣ s := (by norm_num : Nat.Coprime 186 37).mul_dvd_of_dvd_of_dvd hd186 hp37 have hd282162 : 282162 ∣ s := (by norm_num : Nat.Coprime 6882 41).mul_dvd_of_dvd_of_dvd hd6882 hp41 have hle := Nat.le_of_dvd hs hd282162 exact (not_le_of_gt hsbound) ((show 20000 ≤ 282162 by decide).trans hle) by_cases hb4 : b ≤ 83 · have hp83 : 83 ∣ s := hprime 83 (by norm_num) (by omega) (by omega) have hp89 : 89 ∣ s := hprime 89 (by norm_num) (by omega) (by omega) have hd498 : 498 ∣ s := (by norm_num : Nat.Coprime 6 83).mul_dvd_of_dvd_of_dvd h6 hp83 have hd44322 : 44322 ∣ s := (by norm_num : Nat.Coprime 498 89).mul_dvd_of_dvd_of_dvd hd498 hp89 have hle := Nat.le_of_dvd hs hd44322 exact (not_le_of_gt hsbound) ((show 20000 ≤ 44322 by decide).trans hle) by_cases hb5 : b ≤ 241 · have hp241 : 241 ∣ s := hprime 241 (by norm_num) (by omega) (by omega) have hp251 : 251 ∣ s := hprime 251 (by norm_num) (by omega) (by omega) have hd1446 : 1446 ∣ s := (by norm_num : Nat.Coprime 6 241).mul_dvd_of_dvd_of_dvd h6 hp241 have hd362946 : 362946 ∣ s := (by norm_num : Nat.Coprime 1446 251).mul_dvd_of_dvd_of_dvd hd1446 hp251 have hle := Nat.le_of_dvd hs hd362946 exact (not_le_of_gt hsbound) ((show 20000 ≤ 362946 by decide).trans hle) by_cases hb6 : b ≤ 709 · have hp709 : 709 ∣ s := hprime 709 (by norm_num) (by omega) (by omega) have hp719 : 719 ∣ s := hprime 719 (by norm_num) (by omega) (by omega) have hd4254 : 4254 ∣ s := (by norm_num : Nat.Coprime 6 709).mul_dvd_of_dvd_of_dvd h6 hp709 have hd3058626 : 3058626 ∣ s := (by norm_num : Nat.Coprime 4254 719).mul_dvd_of_dvd_of_dvd hd4254 hp719 have hle := Nat.le_of_dvd hs hd3058626 exact (not_le_of_gt hsbound) ((show 20000 ≤ 3058626 by decide).trans hle) by_cases hb7 : b ≤ 2113 · have hp2113 : 2113 ∣ s := hprime 2113 (by norm_num) (by omega) (by omega) have hp2129 : 2129 ∣ s := hprime 2129 (by norm_num) (by omega) (by omega) have hd12678 : 12678 ∣ s := (by norm_num : Nat.Coprime 6 2113).mul_dvd_of_dvd_of_dvd h6 hp2113 have hd26991462 : 26991462 ∣ s := (by norm_num : Nat.Coprime 12678 2129).mul_dvd_of_dvd_of_dvd hd12678 hp2129 have hle := Nat.le_of_dvd hs hd26991462 exact (not_le_of_gt hsbound) ((show 20000 ≤ 26991462 by decide).trans hle) by_cases hb8 : b ≤ 6329 · have hp6329 : 6329 ∣ s := hprime 6329 (by norm_num) (by omega) (by omega) have hp6337 : 6337 ∣ s := hprime 6337 (by norm_num) (by omega) (by omega) have hd37974 : 37974 ∣ s := (by norm_num : Nat.Coprime 6 6329).mul_dvd_of_dvd_of_dvd h6 hp6329 have hd240641238 : 240641238 ∣ s := (by norm_num : Nat.Coprime 37974 6337).mul_dvd_of_dvd_of_dvd hd37974 hp6337 have hle := Nat.le_of_dvd hs hd240641238 exact (not_le_of_gt hsbound) ((show 20000 ≤ 240641238 by decide).trans hle) have hp10007 : 10007 ∣ s := hprime 10007 (by norm_num) (by omega) (by omega) have hp10009 : 10009 ∣ s := hprime 10009 (by norm_num) (by omega) (by omega) have hd60042 : 60042 ∣ s := (by norm_num : Nat.Coprime 6 10007).mul_dvd_of_dvd_of_dvd h6 hp10007 have hd600960378 : 600960378 ∣ s := (by norm_num : Nat.Coprime 60042 10009).mul_dvd_of_dvd_of_dvd hd60042 hp10009 have hle := Nat.le_of_dvd hs hd600960378 exact (not_le_of_gt hsbound) ((show 20000 ≤ 600960378 by decide).trans hle) end Bounty.FiniteArithmetic end /- Proof component: FinitePatterns -/ section namespace Bounty.FiniteArithmetic open Math15.LonelyRunner Bounty.Arithmetic theorem prime_divides_of_window {s b k p : ℕ} (hwindow : ∀ x : ℕ, b ≤ x → x < k * b → 1 < Nat.gcd s x) (hp : Nat.Prime p) (hlo : b ≤ p) (hhi : p < k * b) : p ∣ s := by by_contra hnot have hcop : Nat.gcd s p = 1 := (hp.coprime_iff_not_dvd.mpr hnot).symm.gcd_eq_one have hbad := hwindow p hlo hhi rw [hcop] at hbad omega theorem window_endpoint_le_thirteen {s b k : ℕ} (hs : 0 < s) (hsbound : s < 20000) (hb : b ≤ 4) (h2 : 2 ∣ s) (h3 : 3 ∣ s) (hprime : ∀ p : ℕ, Nat.Prime p → b ≤ p → p < k * b → p ∣ s) : k * b ≤ 13 := by by_contra hnot have h5 : 5 ∣ s := hprime 5 (by norm_num) (by omega) (by omega) have h7 : 7 ∣ s := hprime 7 (by norm_num) (by omega) (by omega) have h11 : 11 ∣ s := hprime 11 (by norm_num) (by omega) (by omega) have h13 : 13 ∣ s := hprime 13 (by norm_num) (by omega) (by omega) have h6 : 6 ∣ s := (by norm_num : Nat.Coprime 2 3).mul_dvd_of_dvd_of_dvd h2 h3 have h30 : 30 ∣ s := (by norm_num : Nat.Coprime 6 5).mul_dvd_of_dvd_of_dvd h6 h5 have h210 : 210 ∣ s := (by norm_num : Nat.Coprime 30 7).mul_dvd_of_dvd_of_dvd h30 h7 have h2310 : 2310 ∣ s := (by norm_num : Nat.Coprime 210 11).mul_dvd_of_dvd_of_dvd h210 h11 have h30030 : 30030 ∣ s := (by norm_num : Nat.Coprime 2310 13).mul_dvd_of_dvd_of_dvd h2310 h13 exact (not_le_of_gt hsbound) ((show 20000 ≤ 30030 by decide).trans (Nat.le_of_dvd hs h30030)) /-- All faster valid replacements in the finite range belong to seven simple divisibility patterns. -/ theorem finite_faster_patterns {n s k : ℕ} (hn : 3 ≤ n) (hnbound : n ≤ 20000) (hs : 0 < s) (hsn : s < n) (hupper : n - 1 < 2 * s) (hk : 3 ≤ k) (hwindow : GcdWindow n s k) : (n - s = 2 ∧ k = 3 ∧ 30 ∣ s) ∨ (n - s = 2 ∧ (k = 4 ∨ k = 5) ∧ 210 ∣ s) ∨ (n - s = 2 ∧ k = 6 ∧ 2310 ∣ s) ∨ (n - s = 3 ∧ k = 3 ∧ 210 ∣ s) ∨ (n - s = 3 ∧ k = 4 ∧ 2310 ∣ s) ∨ (n - s = 4 ∧ k = 3 ∧ 2310 ∣ s) := by let b := n - s have hb2 : 2 ≤ b := gcdWindow_deficit_ge_two hsn (by omega) hwindow have hbsmall : b < s := by have hmid := gcdWindow_above_midpoint hn hsn hupper (by omega) hwindow dsimp [b] omega have hprime : ∀ p : ℕ, Nat.Prime p → b ≤ p → p < k * b → p ∣ s := fun _ hp hlo hhi => prime_divides_of_window hwindow hp hlo hhi have h2 : 2 ∣ s := gcdWindow_prime_support hsn hwindow (by norm_num) (by omega) have h3 : 3 ∣ s := gcdWindow_prime_support hsn hwindow (by norm_num) hk have hsbound : s < 20000 := by omega have hb4 : b ≤ 4 := deficit_le_four hs hsbound hbsmall (by dsimp [b]; omega) h2 h3 (fun p hp hlo hhi => hprime p hp hlo (hhi.trans_le (Nat.mul_le_mul_right b hk))) have hend : k * b ≤ 13 := window_endpoint_le_thirteen hs hsbound hb4 h2 h3 hprime have h5 : 5 ∣ s := hprime 5 (by norm_num) (by omega) (by nlinarith) have h6 : 6 ∣ s := (by norm_num : Nat.Coprime 2 3).mul_dvd_of_dvd_of_dvd h2 h3 have h30 : 30 ∣ s := (by norm_num : Nat.Coprime 6 5).mul_dvd_of_dvd_of_dvd h6 h5 have h210 : 7 < k * b → 210 ∣ s := by intro h7 exact (by norm_num : Nat.Coprime 30 7).mul_dvd_of_dvd_of_dvd h30 (hprime 7 (by norm_num) (by omega) h7) have h2310 : 11 < k * b → 2310 ∣ s := by intro h11 exact (by norm_num : Nat.Coprime 210 11).mul_dvd_of_dvd_of_dvd (h210 (by omega)) (hprime 11 (by norm_num) (by omega) h11) change (b = 2 ∧ k = 3 ∧ 30 ∣ s) ∨ (b = 2 ∧ (k = 4 ∨ k = 5) ∧ 210 ∣ s) ∨ (b = 2 ∧ k = 6 ∧ 2310 ∣ s) ∨ (b = 3 ∧ k = 3 ∧ 210 ∣ s) ∨ (b = 3 ∧ k = 4 ∧ 2310 ∣ s) ∨ (b = 4 ∧ k = 3 ∧ 2310 ∣ s) have hposs : (b = 2 ∧ k = 3) ∨ (b = 2 ∧ (k = 4 ∨ k = 5)) ∨ (b = 2 ∧ k = 6) ∨ (b = 3 ∧ k = 3) ∨ (b = 3 ∧ k = 4) ∨ (b = 4 ∧ k = 3) := by interval_cases b <;> omega rcases hposs with ⟨hb, hk⟩ | ⟨hb, hk⟩ | ⟨hb, hk⟩ | ⟨hb, hk⟩ | ⟨hb, hk⟩ | ⟨hb, hk⟩ · exact Or.inl ⟨hb, hk, h30⟩ · exact Or.inr (Or.inl ⟨hb, hk, h210 (by rcases hk with hk | hk <;> simp [hb, hk])⟩) · exact Or.inr (Or.inr (Or.inl ⟨hb, hk, h2310 (by simp [hb, hk])⟩)) · exact Or.inr (Or.inr (Or.inr (Or.inl ⟨hb, hk, h210 (by simp [hb, hk])⟩))) · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨hb, hk, h2310 (by simp [hb, hk])⟩)))) · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr ⟨hb, hk, h2310 (by simp [hb, hk])⟩)))) end Bounty.FiniteArithmetic end /- Proof component: Certificates -/ section noncomputable section namespace Bounty open Math15.LonelyRunner /-- An exact integer certificate that all speeds are farther than `1/n` from an integer at time `p/q`. -/ def RationalWitness (V : Finset ℕ) (n p q : ℕ) : Prop := 0 < n ∧ 0 < q ∧ ∀ v ∈ V, q < n * min ((v * p) % q) (q - (v * p) % q) theorem rationalWitness_distance_gt {V : Finset ℕ} {n p q : ℕ} (h : RationalWitness V n p q) {v : ℕ} (hv : v ∈ V) : 1 / (n : ℝ) < distance (v • (((p : ℝ) / q : ℝ) : Time)) := by rcases h with ⟨hn, hq, hdist⟩ rw [distance_rational_center] have hnr : (0 : ℝ) < n := by exact_mod_cast hn have hqr : (0 : ℝ) < q := by exact_mod_cast hq apply (div_lt_div_iff₀ hnr hqr).2 simpa only [one_mul, mul_one, mul_comm] using (show (q : ℝ) < n * (min ((v * p) % q) (q - (v * p) % q) : ℕ) by exact_mod_cast hdist v hv) theorem rationalWitness_ML_gt {V : Finset ℕ} {n p q : ℕ} (hV : V.Nonempty) (h : RationalWitness V n p q) : 1 / (n : ℝ) < ML V := by exact ML_gt_of_all_distances_gt hV (fun _ hv => rationalWitness_distance_gt h hv) theorem rationalWitness_not_tight {n r₁ r₂ w₁ w₂ p q : ℕ} (h : RationalWitness (modified n r₁ r₂ w₁ w₂) n p q) : ML (modified n r₁ r₂ w₁ w₂) ≠ 1 / (n : ℝ) := by exact ne_of_gt (rationalWitness_ML_gt (modified_nonempty n r₁ r₂ w₁ w₂) h) end Bounty end end /- Proof component: IntervalCover -/ section noncomputable section namespace Bounty.IntervalCover open Math15.LonelyRunner def GridBad (P c h x : ℝ) : Prop := ∃ k : ℤ, |x - (c + (k : ℝ) * P)| ≤ h theorem right_of_center_bound {a b c P Q hP hQ : ℝ} (k : ℤ) (hP0 : 0 ≤ hP) (hQ0 : 0 ≤ hQ) (hPgap : 2 * hP + 2 * hQ < P) (hQgap : 2 * hQ < Q) (htouch : a ≤ (k : ℝ) * P + hP) (hcover : ∀ x ∈ Set.Icc a b, GridBad P 0 hP x ∨ GridBad Q c hQ x) : b - (k : ℝ) * P ≤ hP + 2 * hQ := by apply two_grid_cover_right_bound (c := c - (k : ℝ) * P) hP0 hQ0 hPgap hQgap intro y hy have hyle : y + (k : ℝ) * P ≤ b := by linarith [hy.2] by_cases hya : a ≤ y + (k : ℝ) * P · rcases hcover (y + (k : ℝ) * P) ⟨hya, hyle⟩ with ⟨j, hj⟩ | ⟨j, hj⟩ · left refine ⟨j - k, ?_⟩ have heq : y - ((j - k : ℤ) : ℝ) * P = y + (k : ℝ) * P - (0 + (j : ℝ) * P) := by push_cast; ring rwa [heq] · right refine ⟨j, ?_⟩ have heq : y - (c - (k : ℝ) * P + (j : ℝ) * Q) = y + (k : ℝ) * P - (c + (j : ℝ) * Q) := by ring rwa [heq] · left refine ⟨0, ?_⟩ simp only [Int.cast_zero, zero_mul, sub_zero, abs_of_nonneg hy.1] linarith theorem reflect_cover {a b c P Q hP hQ : ℝ} (hcover : ∀ x ∈ Set.Icc a b, GridBad P 0 hP x ∨ GridBad Q c hQ x) : ∀ x ∈ Set.Icc (-b) (-a), GridBad P 0 hP x ∨ GridBad Q (-c) hQ x := by intro x hx rcases hcover (-x) ⟨by linarith [hx.2], by linarith [hx.1]⟩ with ⟨j, hj⟩ | ⟨j, hj⟩ · left refine ⟨-j, ?_⟩ have heq : x - (0 + ((-j : ℤ) : ℝ) * P) = -(-x - (0 + (j : ℝ) * P)) := by push_cast ring rwa [heq, abs_neg] · right refine ⟨-j, ?_⟩ have heq : x - (-c + ((-j : ℤ) : ℝ) * Q) = -(-x - (c + (j : ℝ) * Q)) := by push_cast ring rwa [heq, abs_neg] /-- A covered interval has length at most one slower interval plus two faster intervals. This avoids any assumption about finite connected components. -/ theorem two_grid_interval_length {a b c P Q hP hQ : ℝ} (hP0 : 0 ≤ hP) (hQ0 : 0 ≤ hQ) (hPgap : 2 * hP + 2 * hQ < P) (hQgap : 2 * hQ < Q) (hab : a ≤ b) (hcover : ∀ x ∈ Set.Icc a b, GridBad P 0 hP x ∨ GridBad Q c hQ x) : b - a ≤ 2 * hP + 4 * hQ := by by_cases hex : ∃ x ∈ Set.Icc a b, GridBad P 0 hP x · obtain ⟨x, hx, k, hk⟩ := hex have hklo := (abs_le.mp hk).1 have hkhi := (abs_le.mp hk).2 have hright := right_of_center_bound k hP0 hQ0 hPgap hQgap (show a ≤ (k : ℝ) * P + hP by linarith [hx.1]) hcover have hleft := right_of_center_bound (-k) hP0 hQ0 hPgap hQgap (show -b ≤ ((-k : ℤ) : ℝ) * P + hP by push_cast; linarith [hx.2]) (reflect_cover hcover) push_cast at hleft linarith · have hQpos : 0 < Q := by linarith have hQcover : ∀ x ∈ Set.Icc a b, ∃ k : ℤ, |x - (c + (k : ℝ) * Q)| ≤ hQ := by intro x hx rcases hcover x hx with hbad | hbad · exact False.elim (hex ⟨x, hx, hbad⟩) · exact hbad have hh := covered_grid_interval_length hQpos hQgap hab hQcover linarith end Bounty.IntervalCover end end /- Proof component: SmallCases -/ section noncomputable section namespace Bounty.SmallCases open Math15.LonelyRunner IntervalCover Boundary theorem bad_distance_implies_grid {v : ℕ} (hv : 0 < v) {a t : ℝ} (hbad : distance (v • (t : Time)) ≤ a) : GridBad (1 / (v : ℝ)) 0 (a / v) t := by rw [distance, ← AddCircle.coe_nsmul, nsmul_eq_mul, AddCircle.norm_eq] at hbad simp only [inv_one, one_mul, mul_one] at hbad have hv0 : (0 : ℝ) < v := by exact_mod_cast hv refine ⟨round ((v : ℝ) * t), ?_⟩ have heq : t - (0 + (round ((v : ℝ) * t) : ℝ) * (1 / v)) = ((v : ℝ) * t - round ((v : ℝ) * t)) / v := by field_simp; ring rw [heq, abs_div, abs_of_pos hv0] exact div_le_div_of_nonneg_right hbad hv0.le theorem speed_one_good {t : ℝ} (ht : t ∈ Set.Icc (3 / 10 : ℝ) (7 / 10 : ℝ)) : (1 / 4 : ℝ) < distance (1 • (t : Time)) := by by_cases hhalf : t ≤ 1 / 2 · have ht0 : 0 ≤ t := by linarith [ht.1] have hnorm : ‖(t : Time)‖ = |t| := (AddCircle.norm_coe_eq_abs_iff (1 : ℝ) (by norm_num)).2 (by simpa [abs_of_nonneg ht0] using hhalf) simpa [distance, hnorm, abs_of_nonneg ht0] using (show (1 / 4 : ℝ) < t by linarith [ht.1]) · rw [distance_of_integer_sub (z := 1) (a := 1 - t) (by norm_num) (by linarith [ht.2]) (by linarith)] linarith [ht.2] theorem four_runners_ordered {A B : ℕ} (hA : 4 ≤ A) (hB : 4 ≤ B) (hAB : A < B) : (1 / 4 : ℝ) < ML (modified 4 2 3 A B) := by apply lt_of_not_ge intro hML have hA0 : (0 : ℝ) < A := by exact_mod_cast (show 0 < A by omega) have hB0 : (0 : ℝ) < B := by exact_mod_cast (show 0 < B by omega) have hABr : (A : ℝ) < B := by exact_mod_cast hAB have hbase : Finset.Icc 1 (4 - 1 : ℕ) \ {2, 3} = {1} := by decide have hcover : ∀ t ∈ Set.Icc (3 / 10 : ℝ) (7 / 10 : ℝ), GridBad (1 / (A : ℝ)) 0 ((1 / 4 : ℝ) / A) t ∨ GridBad (1 / (B : ℝ)) 0 ((1 / 4 : ℝ) / B) t := by intro t ht obtain ⟨v, hv, hbad⟩ := geometry_exists_distance_le_of_ML_le (modified 4 2 3 A B) ⟨A, by simp [modified]⟩ hML (t : Time) simp only [modified, hbase, Finset.mem_union, Finset.mem_insert, Finset.mem_singleton] at hv rcases hv with rfl | rfl | rfl · exact False.elim ((not_lt_of_ge hbad) (speed_one_good ht)) · exact Or.inl (bad_distance_implies_grid (by omega) hbad) · exact Or.inr (bad_distance_implies_grid (by omega) hbad) have hgapA : 2 * ((1 / 4 : ℝ) / A) + 2 * ((1 / 4 : ℝ) / B) < 1 / A := by field_simp nlinarith have hgapB : 2 * ((1 / 4 : ℝ) / B) < 1 / B := by field_simp linarith have hlength := two_grid_interval_length (by positivity) (by positivity) hgapA hgapB (show (3 / 10 : ℝ) ≤ 7 / 10 by norm_num) hcover have hboundA : ((1 / 4 : ℝ) / A) ≤ (1 / 4) / 4 := div_le_div_of_nonneg_left (by norm_num) (by norm_num) (by exact_mod_cast hA) have hboundB : ((1 / 4 : ℝ) / B) ≤ (1 / 4) / 4 := div_le_div_of_nonneg_left (by norm_num) (by norm_num) (by exact_mod_cast hB) norm_num at hlength hboundA hboundB linarith theorem four_runners {A B : ℕ} (hA : 4 ≤ A) (hB : 4 ≤ B) (hne : A ≠ B) : (1 / 4 : ℝ) < ML (modified 4 2 3 A B) := by rcases lt_or_gt_of_ne hne with h | h · exact four_runners_ordered hA hB h · simpa only [modified, Finset.pair_comm A B] using four_runners_ordered hB hA h theorem no_tight_le_four {n r₁ r₂ A B : ℕ} (hn : 3 ≤ n) (hn4 : n ≤ 4) (hr₁ : 1 ≤ r₁) (hr₁n : r₁ < n) (hr₂ : 1 ≤ r₂) (hr₂n : r₂ < n) (hrne : r₁ ≠ r₂) (hupper₁ : n - 1 < 2 * r₁) (hupper₂ : n - 1 < 2 * r₂) (hA : n ≤ A) (hB : n ≤ B) (hne : A ≠ B) : ML (modified n r₁ r₂ A B) ≠ 1 / (n : ℝ) := by have hn_eq : n = 4 := by omega subst n have hpair : (r₁ = 2 ∧ r₂ = 3) ∨ (r₁ = 3 ∧ r₂ = 2) := by omega have hlarge := four_runners hA hB hne rcases hpair with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ · exact ne_of_gt hlarge · simpa only [modified, Finset.pair_comm 3 2, Nat.cast_ofNat] using ne_of_gt hlarge end Bounty.SmallCases end end /- Proof component: CommonInsertion -/ section noncomputable section namespace Bounty.CommonInsertion open Math15.LonelyRunner Arithmetic Boundary IntervalCover SmallCases theorem common_window_long {n r s m : ℕ} (hr : 0 < r) (hrs : r < s) (hsn : s < n) (hlarge : n ≤ m * r) (hdiv : s ∣ m * r) : n + 2 ≤ m * (n - r) := by obtain ⟨k, hk⟩ := hdiv have hm : 0 < m := by nlinarith have hk2 : 2 ≤ k := by by_contra hnot have hkle : k ≤ 1 := by omega have hmul := Nat.mul_le_mul_left s hkle nlinarith have hkm : k < m := by by_contra hnot have hmk : m ≤ k := by omega have hmul := Nat.mul_le_mul_right s hmk nlinarith have hnmk := Nat.mul_le_mul_left n (show k + 1 ≤ m by omega) have hsubr : n - r + r = n := Nat.sub_add_cancel (by omega) have hsubs : n - s + s = n := Nat.sub_add_cancel (by omega) have hgap : 2 ≤ k * (n - s) := by nlinarith nlinarith theorem centered_shift_distance {r v : ℕ} (hv : r ∣ v) (d : Time) : distance (v • ((((1 / (r : ℝ)) : ℝ) : Time) + d)) = distance (v • d) := by have hzero : v • (((1 / (r : ℝ)) : ℝ) : Time) = 0 := by apply norm_eq_zero.mp change distance (v • (((1 / (r : ℝ)) : ℝ) : Time)) = 0 rw [distance_reciprocal, Nat.mod_eq_zero_of_dvd hv] simp rw [nsmul_add, hzero, zero_add] /-- A uniform hole centered at both inserted grids obeys the component bound. -/ theorem centered_uniform_hole_bound {n r s A B : ℕ} {l : ℝ} (hn : 4 ≤ n) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hA : 0 < A) (hAB : A < B) (hrA : r ∣ A) (hrB : r ∣ B) (hl0 : 0 ≤ l) (hlhalf : l ≤ 1 / 2) (hl : (n - 1 : ℕ) * l < 1 / (r : ℝ) - 1 / (n : ℝ)) (hML : ML (modified n r s A B) ≤ 1 / (n : ℝ)) : l ≤ (1 / (n : ℝ)) / A + 2 * ((1 / (n : ℝ)) / B) := by have hn0 : (0 : ℝ) < n := by exact_mod_cast (show 0 < n by omega) have hA0 : (0 : ℝ) < A := by exact_mod_cast hA have hB0 : (0 : ℝ) < B := by exact_mod_cast (show 0 < B by omega) have hABr : (A : ℝ) < B := by exact_mod_cast hAB have hnr : (4 : ℝ) ≤ n := by exact_mod_cast hn have hgapA : 2 * ((1 / (n : ℝ)) / A) + 2 * ((1 / (n : ℝ)) / B) < 1 / A := by field_simp nlinarith have hgapB : 2 * ((1 / (n : ℝ)) / B) < 1 / B := by field_simp nlinarith apply two_grid_cover_right_bound (c := 0) (by positivity) (by positivity) hgapA hgapB intro d hd have hdhalf : d ≤ 1 / 2 := hd.2.trans hlhalf have hnorm : distance (d : Time) = d := by change ‖(d : Time)‖ = d have hh := (AddCircle.norm_coe_eq_abs_iff (1 : ℝ) (by norm_num)).2 (show |d| ≤ |(1 : ℝ)| / 2 by simpa only [abs_one, abs_of_nonneg hd.1] using hdhalf) simpa only [abs_of_nonneg hd.1] using hh have hsmall : (n - 1 : ℕ) * distance (d : Time) < 1 / (r : ℝ) - 1 / (n : ℝ) := by rw [hnorm] exact (mul_le_mul_of_nonneg_left hd.2 (by positivity)).trans_lt hl have hcov := insertion_covers_near_primitive_center n r s A B 1 (d : Time) hr hrn hupper (by simp) hML hsmall simp only [Nat.cast_one, centered_shift_distance hrA, centered_shift_distance hrB] at hcov rcases hcov with hcov | hcov · left obtain ⟨k, hk⟩ := bad_distance_implies_grid hA hcov exact ⟨k, by simpa only [zero_add] using hk⟩ · right exact bad_distance_implies_grid (by omega) hcov end Bounty.CommonInsertion end end /- Proof component: CommonPair -/ section noncomputable section namespace Bounty.CommonInsertion open Math15.LonelyRunner Arithmetic Boundary theorem opposite_units_in_long_window {n r T : ℕ} (hn : 4 ≤ n) (hrn : r < n) (hupper : n - 1 < 2*r) (hT : n+2 ≤ T) : ∃ u v : ℕ, n-r ≤ u ∧ u ring have he : (r:ℤ)∣E+B := by convert dvd_sub (dvd_mul_of_dvd_right hv' E) hEdiv using 1 <;> ring have hde : (r:ℤ)∣D+E := by convert dvd_add hd he using 1 <;> ring have hrle : (r:ℤ)≤D+E := Int.le_of_dvd (by omega) hde have hsum := mul_le_mul_of_nonneg_left hrle (show (0:ℤ)≤(n:ℤ)*m by positivity) have hDhi := (abs_le.mp hDb).2 have hEhi := (abs_le.mp hEb).2 have hbound : ((n:ℤ)-2)*((m:ℤ)*r) ≤ 2*B := by nlinarith constructor · have hn2 : 2≤n := by omega exact_mod_cast hbound · have hn4 : (4:ℤ)≤n := by exact_mod_cast hn have hle : (m:ℤ)*r ≤ B := by nlinarith have hne : m*r≠B := by intro hh; apply hnot; rw [←hh]; exact Nat.dvd_mul_left r m exact lt_of_le_of_ne (by exact_mod_cast hle) hne theorem common_exclusive_other_large {n r s m B : ℕ} (hn : 4≤n) (hr : 0 dsimp [D] <;> ring · have hden : (0 : ℝ) < (n : ℝ) * m * r * B := by positivity have heq : (1 / ((n : ℝ) * m * r) - ((p : ℝ) / r + (k : ℝ) * (1 / (B : ℝ)))) * ((n : ℝ) * m * r * B) = -((n : ℝ) * m * (D : ℝ) - B) := by dsimp [D] push_cast field_simp ring have hbound : |(n : ℝ) * m * (D : ℝ) - B| ≤ (m : ℝ) * r := by calc |(n : ℝ) * m * (D : ℝ) - B| = |(1 / ((n : ℝ) * m * r) - ((p : ℝ) / r + (k : ℝ) * (1 / (B : ℝ)))) * ((n : ℝ) * m * r * B)| := by rw [heq, abs_neg] _ = |1 / ((n : ℝ) * m * r) - ((p : ℝ) / r + (k : ℝ) * (1 / (B : ℝ)))| * ((n : ℝ) * m * r * B) := by rw [abs_mul, abs_of_pos hden] _ ≤ ((1 / (n : ℝ)) / B) * ((n : ℝ) * m * r * B) := mul_le_mul_of_nonneg_right hk hden.le _ = (m : ℝ) * r := by field_simp exact_mod_cast hbound · have hden : (0 : ℝ) < (n : ℝ) * r * x * B := by positivity have hh := mul_le_mul_of_nonneg_right hreach hden.le have heqL : ((1 / (r : ℝ) - 1 / (n : ℝ)) / x) * ((n : ℝ) * r * x * B) = ((n - r : ℕ) : ℝ) * B := by rw [Nat.cast_sub (show r ≤ n by omega)] field_simp have heqR : ((p : ℝ) / r + (k : ℝ) * (1 / (B : ℝ)) + (1 / (n : ℝ)) / B) * ((n : ℝ) * r * x * B) = (x : ℝ) * ((n : ℝ) * (D : ℝ) + r) := by dsimp [D] push_cast field_simp rw [heqL, heqR] at hh exact_mod_cast hh /-- The two-grid reach estimate also applies to an interval open at its right endpoint. -/ theorem two_grid_cover_Ico_right_bound {H c P Q hP hQ : ℝ} (hP0 : 0 ≤ hP) (hQ0 : 0 ≤ hQ) (hPgap : 2 * hP + 2 * hQ < P) (hQgap : 2 * hQ < Q) (hcover : ∀ u ∈ Set.Ico 0 H, (∃ k : ℤ, |u - (k : ℝ) * P| ≤ hP) ∨ (∃ j : ℤ, |u - (c + (j : ℝ) * Q)| ≤ hQ)) : H ≤ hP + 2 * hQ := by by_contra! hbig let b := (H + (hP + 2 * hQ)) / 2 have hb : b < H := by dsimp [b]; linarith have hreach : b ≤ hP + 2 * hQ := two_grid_cover_right_bound hP0 hQ0 hPgap hQgap (fun u hu => hcover u ⟨hu.1, hu.2.trans_lt hb⟩) dsimp [b] at hreach linarith /-- A centered acceleration's bad set has a grid center at the primitive removed-speed center. -/ theorem acceleration_bad_implies_centered_grid {n m r p : ℕ} {u : ℝ} (hm : 0 < m) (hr : 0 < r) (hbad : distance ((m * r) • ((((p : ℝ) / r - u) : ℝ) : Time)) ≤ 1 / (n : ℝ)) : ∃ k : ℤ, |u - (k : ℝ) * (1 / ((m * r : ℕ) : ℝ))| ≤ (1 / (n : ℝ)) / (m * r : ℕ) := by have hm0 : (0 : ℝ) < m := by exact_mod_cast hm have hr0 : (0 : ℝ) < r := by exact_mod_cast hr obtain ⟨k, hk⟩ := bad_implies_grid_interval (Nat.mul_pos hm hr) hbad refine ⟨k + (m * p : ℕ), ?_⟩ have heq : ((k + (m * p : ℕ) : ℤ) : ℝ) * (1 / ((m * r : ℕ) : ℝ)) = (p : ℝ) / r + (k : ℝ) * (1 / ((m * r : ℕ) : ℝ)) := by push_cast field_simp ring simpa only [heq] using hk /-- The exact local-hole extent is bounded by the centered slower interval's radius plus twice the faster interval's radius. -/ theorem sharp_left_hole_reach_bound {n r s m p x B : ℕ} (hn : 4 ≤ n) (hr : 0 < r) (hrn : r < n) (hupper : n - 1 < 2 * r) (hm : 0 < m) (hfast : m * r < B) (hcop : Nat.Coprime p r) (hpx : Nat.ModEq r (p * x) 1) (hxlo : n - r ≤ x) (hML : ML (modified n r s (m * r) B) ≤ 1 / (n : ℝ)) : (1 / (r : ℝ) - 1 / (n : ℝ)) / x ≤ 1 / ((n : ℝ) * (m * r : ℕ)) + 2 / ((n : ℝ) * B) := by have hn0 : (0 : ℝ) < n := by exact_mod_cast (show 0 < n by omega) have hm0 : (0 : ℝ) < m := by exact_mod_cast hm have hr0 : (0 : ℝ) < r := by exact_mod_cast hr have hA0 : (0 : ℝ) < (m * r : ℕ) := by positivity have hB0 : (0 : ℝ) < B := by exact_mod_cast (show 0 < B by nlinarith) have hn4 : (4 : ℝ) ≤ n := by exact_mod_cast hn have hAB : ((m * r : ℕ) : ℝ) < B := by exact_mod_cast hfast have hgapA : 2 * ((1 / (n : ℝ)) / (m * r : ℕ)) + 2 * ((1 / (n : ℝ)) / B) < 1 / ((m * r : ℕ) : ℝ) := by have hd : 0 < (n : ℝ) * (m * r : ℕ) * B := by positivity apply (mul_lt_mul_iff_right₀ hd).mp have heqL : (2 * ((1 / (n : ℝ)) / (m * r : ℕ)) + 2 * ((1 / (n : ℝ)) / B)) * ((n : ℝ) * (m * r : ℕ) * B) = 2 * B + 2 * (m * r : ℕ) := by field_simp have heqR : (1 / ((m * r : ℕ) : ℝ)) * ((n : ℝ) * (m * r : ℕ) * B) = (n : ℝ) * B := by field_simp rw [mul_comm ((n : ℝ) * (m * r : ℕ) * B), heqL, mul_comm ((n : ℝ) * (m * r : ℕ) * B), heqR] nlinarith have hgapB : 2 * ((1 / (n : ℝ)) / B) < 1 / (B : ℝ) := by have hh : 2 * (1 / (n : ℝ)) < 1 := by have hni : 2 / (n : ℝ) < 1 := (div_lt_one hn0).mpr (by linarith) simpa only [mul_one_div] using hni calc 2 * ((1 / (n : ℝ)) / B) = (2 * (1 / (n : ℝ))) / B := by ring _ < 1 / (B : ℝ) := div_lt_div_of_pos_right hh hB0 have hcover : ∀ u ∈ Set.Ico 0 ((1 / (r : ℝ) - 1 / (n : ℝ)) / x), (∃ k : ℤ, |u - (k : ℝ) * (1 / ((m * r : ℕ) : ℝ))| ≤ (1 / (n : ℝ)) / (m * r : ℕ)) ∨ (∃ j : ℤ, |u - ((p : ℝ) / r + (j : ℝ) * (1 / (B : ℝ)))| ≤ (1 / (n : ℝ)) / B) := by intro u hu have hV : (modified n r s (m * r) B).Nonempty := by refine ⟨B, ?_⟩ simp [modified] obtain ⟨v, hv, hbad⟩ := geometry_exists_distance_le_of_ML_le _ hV hML ((((p : ℝ) / r - u) : ℝ) : Time) simp only [modified, Finset.mem_union, Finset.mem_sdiff, Finset.mem_Icc, Finset.mem_insert, Finset.mem_singleton] at hv rcases hv with ⟨⟨hvpos, hvn⟩, hvr⟩ | rfl | rfl · have hgood := retained_good_before_left_extent (by omega) hr hrn hupper hcop hpx hxlo (show 0 < v by omega) (show v < n by omega) (show v ≠ r by intro hh; exact hvr (Or.inl hh)) hu.1 hu.2 exact False.elim ((not_lt_of_ge hbad) hgood) · exact Or.inl (acceleration_bad_implies_centered_grid hm hr hbad) · exact Or.inr (bad_implies_grid_interval (by exact_mod_cast hB0) hbad) have hresult := two_grid_cover_Ico_right_bound (by positivity) (by positivity) hgapA hgapB hcover simpa only [div_div, mul_one_div, ← mul_div_assoc, mul_one] using hresult end Bounty.Boundary end end /- Proof component: CoprimeRemoval -/ section noncomputable section namespace Bounty.CoprimeRemoval open Math15.LonelyRunner Bounty.IntervalCover Bounty.SmallCases /-- When an interval joins a center of the slower grid to a center of the faster grid, complete coverage forces the two centered bad intervals to meet. -/ theorem centered_grid_bridge {b P Q hP hQ : ℝ} (_hb : 0 ≤ b) (hP0 : 0 ≤ hP) (hQ0 : 0 ≤ hQ) (hPgap : 2 * hP + 2 * hQ < P) (hQgap : 2 * hQ < Q) (hcover : ∀ x ∈ Set.Icc 0 b, GridBad P 0 hP x ∨ GridBad Q b hQ x) : b ≤ hP + hQ := by have hbound : b ≤ hP + 2 * hQ := by apply two_grid_cover_right_bound (c := b) hP0 hQ0 hPgap hQgap intro x hx simpa [GridBad] using hcover x hx by_contra hnot have hsum : hP + hQ < b := by linarith let x := (max hP (b - Q + hQ) + (b - hQ)) / 2 have hmax : max hP (b - Q + hQ) < b - hQ := by exact max_lt (by linarith) (by linarith) have hxleft : max hP (b - Q + hQ) < x := by dsimp [x]; linarith have hxright : x < b - hQ := by dsimp [x]; linarith have hxP : hP < x := lt_of_le_of_lt (le_max_left _ _) hxleft have hxQ : b - Q + hQ < x := lt_of_le_of_lt (le_max_right _ _) hxleft have hxmem : x ∈ Set.Icc 0 b := ⟨by linarith, by linarith⟩ have hPpos : 0 < P := by linarith have hQpos : 0 < Q := by linarith rcases hcover x hxmem with hp | hq · apply (between_grid_intervals hPpos (0 : ℤ) (by simpa using hxP) ?_) hp norm_num linarith · apply (between_grid_intervals hQpos (-1 : ℤ) (by norm_num; linarith) ?_) hq norm_num linarith /-- Translation of `centered_grid_bridge` to arbitrary endpoint centers. -/ theorem centered_grid_bridge_translated {a b P Q hP hQ : ℝ} {i j : ℤ} (hab : a ≤ b) (ha : a = (i : ℝ) * P) (hb : b = (j : ℝ) * Q) (hP0 : 0 ≤ hP) (hQ0 : 0 ≤ hQ) (hPgap : 2 * hP + 2 * hQ < P) (hQgap : 2 * hQ < Q) (hcover : ∀ x ∈ Set.Icc a b, GridBad P 0 hP x ∨ GridBad Q 0 hQ x) : b - a ≤ hP + hQ := by apply centered_grid_bridge (by linarith) hP0 hQ0 hPgap hQgap intro x hx rcases hcover (x + a) ⟨by linarith [hx.1], by linarith [hx.2]⟩ with ⟨z, hz⟩ | ⟨z, hz⟩ · left refine ⟨z - i, ?_⟩ have heq : x - (0 + ((z - i : ℤ) : ℝ) * P) = x + a - (0 + (z : ℝ) * P) := by rw [ha] push_cast ring rwa [heq] · right refine ⟨z - j, ?_⟩ have heq : x - (b - a + ((z - j : ℤ) : ℝ) * Q) = x + a - (0 + (z : ℝ) * Q) := by rw [hb] push_cast ring rwa [heq] /-- Farey adjacency: an integer point cannot lie between these two fractions when its denominator is smaller than the sum of their denominators. -/ theorem retained_good_on_unimodular_interval {n r s v : ℕ} {p q : ℤ} {t : ℝ} (_hn : 0 < n) (hr : 0 < r) (hs : 0 < s) (hrn : r < n) (hsn : s < n) (hv : v < r + s) (hvr : ¬ r ∣ v) (hvs : ¬ s ∣ v) (hdet : q * (r : ℤ) - p * (s : ℤ) = 1) (ht : t ∈ Set.Icc ((p : ℝ) / r) ((q : ℝ) / s)) : 1 / (n : ℝ) < distance (v • (t : Time)) := by let z : ℤ := round ((v : ℝ) * t) let e : ℤ := z * r - (v : ℤ) * p let f : ℤ := (v : ℤ) * q - z * s have hid : e * s + f * r = (v : ℤ) := by dsimp [e, f] nlinarith [hdet] have her : e ≠ 0 := by intro he apply hvr apply Int.natCast_dvd_natCast.mp refine ⟨f, ?_⟩ rw [he, zero_mul, zero_add] at hid nlinarith [hid] have hfs : f ≠ 0 := by intro hf apply hvs apply Int.natCast_dvd_natCast.mp refine ⟨e, ?_⟩ rw [hf, zero_mul, add_zero] at hid nlinarith [hid] have hsign : e ≤ -1 ∨ f ≤ -1 := by by_contra! hnot have he : 1 ≤ e := by omega have hf : 1 ≤ f := by omega have hrz : (0 : ℤ) < r := by exact_mod_cast hr have hsz : (0 : ℤ) < s := by exact_mod_cast hs have hvz : (v : ℤ) < (r : ℤ) + s := by exact_mod_cast hv nlinarith have hrr : (0 : ℝ) < r := by exact_mod_cast hr have hsr : (0 : ℝ) < s := by exact_mod_cast hs have hvr0 : (0 : ℝ) ≤ v := by positivity rw [distance, ← AddCircle.coe_nsmul, nsmul_eq_mul, AddCircle.norm_eq] simp only [inv_one, one_mul, mul_one] change 1 / (n : ℝ) < |(v : ℝ) * t - (z : ℝ)| rcases hsign with he | hf · have he' : (1 : ℝ) ≤ (v : ℝ) * p - (z : ℝ) * r := by have h : (1 : ℤ) ≤ (v : ℤ) * p - z * r := by dsimp [e] at he; omega exact_mod_cast h have hlo : (p : ℝ) ≤ t * r := (div_le_iff₀ hrr).mp ht.1 have hmul := mul_le_mul_of_nonneg_left hlo hvr0 have hdist : 1 / (r : ℝ) ≤ (v : ℝ) * t - (z : ℝ) := by apply (div_le_iff₀ hrr).mpr nlinarith have hrecip : 1 / (n : ℝ) < 1 / (r : ℝ) := one_div_lt_one_div_of_lt hrr (by exact_mod_cast hrn) exact (hrecip.trans_le hdist).trans_le (le_abs_self _) · have hf' : (1 : ℝ) ≤ (z : ℝ) * s - (v : ℝ) * q := by have h : (1 : ℤ) ≤ z * s - (v : ℤ) * q := by dsimp [f] at hf; omega exact_mod_cast h have hhi : t * s ≤ (q : ℝ) := (le_div_iff₀ hsr).mp ht.2 have hmul := mul_le_mul_of_nonneg_left hhi hvr0 have hdist : 1 / (s : ℝ) ≤ (z : ℝ) - (v : ℝ) * t := by apply (div_le_iff₀ hsr).mpr nlinarith have hrecip : 1 / (n : ℝ) < 1 / (s : ℝ) := one_div_lt_one_div_of_lt hsr (by exact_mod_cast hsn) have habs : (z : ℝ) - (v : ℝ) * t ≤ |(v : ℝ) * t - (z : ℝ)| := by simpa only [neg_sub] using neg_le_abs ((v : ℝ) * t - (z : ℝ)) exact (hrecip.trans_le hdist).trans_le habs /-- Two matched accelerations with coprime upper-half removals cannot cover the retained-good Farey interval. The faster insertion can also be a common multiple: the centered-grid argument includes that case automatically. -/ theorem coprime_matched_impossible_ordered {n r s m k : ℕ} (hn : 5 ≤ n) (hr : 0 < r) (hs : 0 < s) (hrn : r < n) (hsn : s < n) (hupperr : n - 1 < 2 * r) (huppers : n - 1 < 2 * s) (hm : 2 ≤ m) (hk : 2 ≤ k) (hfast : m * r < k * s) (hML : ML (modified n r s (m * r) (k * s)) ≤ 1 / (n : ℝ)) : ¬ Nat.Coprime r s := by intro hcop let p : ℤ := -Nat.gcdB r s let q : ℤ := Nat.gcdA r s have hdet : q * (r : ℤ) - p * (s : ℤ) = 1 := by have hbez := Nat.gcd_eq_gcd_ab r s rw [hcop.gcd_eq_one] at hbez dsimp [p, q] push_cast at hbez nlinarith [hbez] let a : ℝ := (p : ℝ) / r let b : ℝ := (q : ℝ) / s have hn0 : (0 : ℝ) < n := by exact_mod_cast (show 0 < n by omega) have hr0 : (0 : ℝ) < r := by exact_mod_cast hr have hs0 : (0 : ℝ) < s := by exact_mod_cast hs have hm0 : (0 : ℝ) < m := by exact_mod_cast (show 0 < m by omega) have hk0 : (0 : ℝ) < k := by exact_mod_cast (show 0 < k by omega) have hnr : (5 : ℝ) ≤ n := by exact_mod_cast hn have hmr : (2 : ℝ) ≤ m := by exact_mod_cast hm have hkr : (2 : ℝ) ≤ k := by exact_mod_cast hk have hrrn : (r : ℝ) < n := by exact_mod_cast hrn have hsrn : (s : ℝ) < n := by exact_mod_cast hsn have hfastr : (m : ℝ) * r < (k : ℝ) * s := by exact_mod_cast hfast have hdetr : (q : ℝ) * r - (p : ℝ) * s = 1 := by exact_mod_cast hdet have hlength : b - a = 1 / ((r : ℝ) * s) := by dsimp [a, b] field_simp nlinarith [hdetr] have hab : a ≤ b := by rw [← sub_nonneg, hlength]; positivity have hcover : ∀ t ∈ Set.Icc a b, GridBad (1 / ((m : ℝ) * r)) 0 ((1 / (n : ℝ)) / ((m : ℝ) * r)) t ∨ GridBad (1 / ((k : ℝ) * s)) 0 ((1 / (n : ℝ)) / ((k : ℝ) * s)) t := by intro t ht obtain ⟨v, hv, hbad⟩ := geometry_exists_distance_le_of_ML_le (modified n r s (m * r) (k * s)) ⟨m * r, by simp [modified]⟩ hML (t : Time) simp only [modified, Finset.mem_union, Finset.mem_sdiff, Finset.mem_Icc, Finset.mem_insert, Finset.mem_singleton] at hv rcases hv with ⟨⟨hvpos, hvn⟩, hvnot⟩ | rfl | rfl · have hvr : ¬ r ∣ v := by intro hd have heq : v = r := Nat.eq_of_dvd_of_lt_two_mul (by omega) hd (by omega) exact hvnot (Or.inl heq) have hvs : ¬ s ∣ v := by intro hd have heq : v = s := Nat.eq_of_dvd_of_lt_two_mul (by omega) hd (by omega) exact hvnot (Or.inr heq) have hgood := retained_good_on_unimodular_interval (by omega) hr hs hrn hsn (by omega : v < r + s) hvr hvs hdet ht exact False.elim ((not_lt_of_ge hbad) hgood) · left simpa only [Nat.cast_mul] using bad_distance_implies_grid (show 0 < m * r by positivity) hbad · right simpa only [Nat.cast_mul] using bad_distance_implies_grid (show 0 < k * s by positivity) hbad have hgapP : 2 * ((1 / (n : ℝ)) / ((m : ℝ) * r)) + 2 * ((1 / (n : ℝ)) / ((k : ℝ) * s)) < 1 / ((m : ℝ) * r) := by have hks : (0 : ℝ) < (k : ℝ) * s := mul_pos hk0 hs0 have hmul := mul_le_mul_of_nonneg_right hnr hks.le field_simp nlinarith only [hfastr, hmul, hks] have hgapQ : 2 * ((1 / (n : ℝ)) / ((k : ℝ) * s)) < 1 / ((k : ℝ) * s) := by field_simp nlinarith have ha : a = (((m : ℤ) * p : ℤ) : ℝ) * (1 / ((m : ℝ) * r)) := by dsimp [a] push_cast field_simp have hb : b = (((k : ℤ) * q : ℤ) : ℝ) * (1 / ((k : ℝ) * s)) := by dsimp [b] push_cast field_simp have hbound := centered_grid_bridge_translated hab ha hb (by positivity) (by positivity) hgapP hgapQ hcover have hA : (1 / (n : ℝ)) / ((m : ℝ) * r) ≤ (1 / (n : ℝ)) / (2 * r) := div_le_div_of_nonneg_left (by positivity) (by positivity) (by nlinarith) have hB : (1 / (n : ℝ)) / ((k : ℝ) * s) ≤ (1 / (n : ℝ)) / (2 * s) := div_le_div_of_nonneg_left (by positivity) (by positivity) (by nlinarith) have hsmall : (1 / (n : ℝ)) / (2 * r) + (1 / (n : ℝ)) / (2 * s) < 1 / ((r : ℝ) * s) := by field_simp nlinarith rw [hlength] at hbound linarith /-- The coprime-removal exclusion with no ordering on the matched insertions. -/ theorem gcd_gt_one_of_matched_multipliers {n r s m k : ℕ} (hn : 5 ≤ n) (hr : 0 < r) (hs : 0 < s) (hrn : r < n) (hsn : s < n) (hupperr : n - 1 < 2 * r) (huppers : n - 1 < 2 * s) (hm : 2 ≤ m) (hk : 2 ≤ k) (hne : m * r ≠ k * s) (hML : ML (modified n r s (m * r) (k * s)) ≤ 1 / (n : ℝ)) : 1 < Nat.gcd r s := by have hnot : ¬ Nat.Coprime r s := by rcases lt_or_gt_of_ne hne with hfast | hfast · exact coprime_matched_impossible_ordered hn hr hs hrn hsn hupperr huppers hm hk hfast hML · have hML' : ML (modified n s r (k * s) (m * r)) ≤ 1 / (n : ℝ) := by simpa only [modified, Finset.pair_comm s r, Finset.pair_comm (k * s) (m * r)] using hML intro hcop exact coprime_matched_impossible_ordered hn hs hr hsn hrn huppers hupperr hk hm hfast hML' hcop.symm have hpos : 0 < Nat.gcd r s := Nat.gcd_pos_of_pos_left s hr change ¬ Nat.gcd r s = 1 at hnot omega /-- Divisibility matching suffices for coprime-removal exclusion. -/ theorem gcd_gt_one_of_matching {n r s A B : ℕ} (hn : 5 ≤ n) (hr : 0 < r) (hs : 0 < s) (hrn : r < n) (hsn : s < n) (hupperr : n - 1 < 2 * r) (huppers : n - 1 < 2 * s) (hA : n ≤ A) (hB : n ≤ B) (hne : A ≠ B) (hAr : r ∣ A) (hBs : s ∣ B) (hML : ML (modified n r s A B) ≤ 1 / (n : ℝ)) : 1 < Nat.gcd r s := by obtain ⟨m, hmA⟩ := hAr obtain ⟨k, hkB⟩ := hBs have hm : 2 ≤ m := by by_contra hnot have hle : m ≤ 1 := by omega nlinarith have hk : 2 ≤ k := by by_contra hnot have hle : k ≤ 1 := by omega nlinarith have hAe : A = m * r := by nlinarith [hmA] have hBe : B = k * s := by nlinarith [hkB] subst A B exact gcd_gt_one_of_matched_multipliers hn hr hs hrn hsn hupperr huppers hm hk (by simpa only [mul_comm r m, mul_comm s k] using hne) (by simpa only [mul_comm r m, mul_comm s k] using hML) end Bounty.CoprimeRemoval end end /- Proof component: CommonForce -/ section noncomputable section namespace Bounty.CommonInsertion open Math15.LonelyRunner Arithmetic Boundary theorem common_forces_smaller_divisor {n r s A B:ℕ} (hn : 5≤n) (hr : 0 rcases hsdiv with hsA | hsB · rcases lt_or_gt_of_ne hrs with hlt | hlt · exact Or.inr ⟨common_forces_smaller_divisor hn hr hlt hsn hupperr hA hrA hsA hML,hsA⟩ · exact Or.inl ⟨hrA,common_forces_smaller_divisor hn hs hlt hrn huppers hA hsA hrA hMLs⟩ · exact Or.inl ⟨hrA,hsB⟩ · exact Or.inr ⟨hrB,hsA⟩ · have hMLB : ML (modified n r s B A) ≤ 1/(n:ℝ) := by simpa only [modified, Finset.pair_comm B A] using hML have hMLBs : ML (modified n s r B A) ≤ 1/(n:ℝ) := by simpa only [modified, Finset.pair_comm s r] using hMLB rcases lt_or_gt_of_ne hrs with hlt | hlt · exact Or.inl ⟨common_forces_smaller_divisor hn hr hlt hsn hupperr hB hrB hsB hMLB,hsB⟩ · exact Or.inr ⟨hrB,common_forces_smaller_divisor hn hs hlt hrn huppers hB hsB hrB hMLBs⟩ theorem removals_gcd_gt_one {n r s A B:ℕ} (hn : 5≤n) (hr : 0 ring have hsmallDiff : |((k:ℤ)*((s:ℤ)-r))-((D:ℤ)*x)| < r := by have hsubr' : (n:ℤ)-r=(n-r:ℕ) := by omega have hsubs' : (n:ℤ)-s=(n-s:ℕ) := by omega have hka' : 4*((k:ℤ)*(n-r:ℕ)) nlinarith have hid : (D:ℤ)*x=(k:ℤ)*((s:ℤ)-r) := by have hz : ((k:ℤ)*((s:ℤ)-r))-((D:ℤ)*x)=0 := Int.eq_zero_of_dvd_of_natAbs_lt_natAbs hmod.dvd (by have hh : (Int.natAbs (((k:ℤ)*((s:ℤ)-r))-((D:ℤ)*x)):ℤ) (n:ℤ)*y) hid have hbound : ((k:ℤ)*((n:ℤ)-s))*(r:ℤ) ≤ (x:ℤ)*r := by nlinarith only [hflankz,hprod] have hh := (mul_le_mul_iff_left₀ hrz).mp hbound rw [←Nat.cast_sub hsn.le] at hh exact_mod_cast hh exact ⟨hsr',hnat,hkbx,fun y hylo hyhi hy => hu y x hylo hyhi hy hxlo hxhi hxr⟩ end Bounty.NoWrap end end /- Proof component: FullResidue -/ section noncomputable section namespace Bounty.Boundary open Math15.LonelyRunner Arithmetic theorem common_residue_full_flank {n r s m B D x:ℕ} (hn : 3≤n) (hr : 0 gcdWindow_prime_support hsn hw hp hpk have hδa : s-r+(n-s)=n-r := by omega obtain ⟨h,hm2,hkthree,hDtwo,hgcd2,hδ,hx3,hbh,hhr,hhs⟩ := Bounty.MixedCase.doubling_tripling_of_unique_unit (show 0 hsA (heq ▸ (by simpa only [hAe] using (Nat.dvd_mul_left r m)))) (by simpa only [←hBe] using hrB) (by simpa only [←hAe] using hsA) hkw (by simpa only [←hAe,←hBe] using hML) exact ⟨⟨m,by omega,hAe,hmw⟩,⟨k,by omega,hBe,hkw⟩⟩ theorem exclusive_matched_conditions (H:RemainingWindowAssertion) {n r s A B:ℕ} (hn:5≤n) (hr:0 hcommonB ⟨h,hh.2⟩) (fun h => hcommonA ⟨hh.1,h⟩) hle) · have hML' : ML (modified n r s B A)≤1/(n:ℝ) := by simpa only [modified,Finset.pair_comm B A] using hle exact Or.inr (exclusive_matched_conditions H hn5 hr hs hrn hsn hupperr huppers hB hA hAB.symm hh.1 hh.2 (fun h => hcommonA ⟨h,hh.2⟩) (fun h => hcommonB ⟨hh.1,h⟩) hML') end Bounty.Classification end end /- Proof component: Kanold -/ section /-! An elementary sieve bound for gaps between integers coprime to a modulus. The bound proved here will be `(ω(r)+1)*2^ω(r)`, rather than Kanold's sharper `2^ω(r)`. The latter's original proof uses substantial prime estimates. -/ namespace Bounty.CoprimeGaps open Finset private abbrev Avoids (S : Finset ℕ) (x : ℕ) : Prop := ∀ p ∈ S, ¬ p ∣ x private theorem avoids_product (S : Finset ℕ) (x : ℕ) : (∏ p ∈ S, (1 - (if p ∣ x then 1 else 0) : ℚ)) = if Avoids S x then 1 else 0 := by classical induction S using Finset.induction_on with | empty => simp [Avoids] | @insert p S hp ih => rw [Finset.prod_insert hp, ih] by_cases hpx : p ∣ x <;> by_cases hS : Avoids S x <;> simp_all [Avoids] private theorem divisibility_product (S : Finset ℕ) (x : ℕ) (hS : ∀ p ∈ S, Nat.Prime p) : (∏ p ∈ S, (if p ∣ x then 1 else 0 : ℚ)) = if (∏ p ∈ S, p) ∣ x then 1 else 0 := by classical by_cases hall : ∀ p ∈ S, p ∣ x · have hdiv : (∏ p ∈ S, p) ∣ x := Finset.prod_primes_dvd x (fun p hp ↦ (hS p hp).prime) hall simp only [hdiv, ite_true] apply Finset.prod_eq_one intro p hp simp [hall p hp] · push Not at hall obtain ⟨p, hp, hnot⟩ := hall have hdiv : ¬ (∏ q ∈ S, q) ∣ x := by intro h exact hnot (dvd_trans (Finset.dvd_prod_of_mem id hp) h) rw [ite_eq_right hdiv] exact Finset.prod_eq_zero hp (by simp [hnot]) private theorem sieve_indicator (S : Finset ℕ) (x : ℕ) (hS : ∀ p ∈ S, Nat.Prime p) : (if Avoids S x then 1 else 0 : ℚ) = ∑ T ∈ S.powerset, (-1 : ℚ) ^ T.card * (if (∏ p ∈ T, p) ∣ x then 1 else 0) := by classical rw [← avoids_product] rw [Finset.prod_sub] apply Finset.sum_congr rfl intro T hT have hTS : T ⊆ S := Finset.mem_powerset.mp hT simp only [Finset.prod_const_one, mul_one] rw [divisibility_product T x (fun p hp ↦ hS p (hTS hp))] private theorem multiples_count {a b d : ℕ} (hab : a ≤ b) : (((Ioc a b).filter fun x ↦ d ∣ x).card : ℚ) = (b / d : ℕ) - (a / d : ℕ) := by have heq : (Ioc a b).filter (fun x ↦ d ∣ x) = ((Ioc 0 b).filter fun x ↦ d ∣ x) \ ((Ioc 0 a).filter fun x ↦ d ∣ x) := by ext x simp only [mem_filter, mem_Ioc, mem_sdiff] omega have hsubset : ((Ioc 0 a).filter fun x ↦ d ∣ x) ⊆ ((Ioc 0 b).filter fun x ↦ d ∣ x) := by intro x hx simp only [mem_filter, mem_Ioc] at hx ⊢ omega rw [heq, Finset.card_sdiff_of_subset hsubset, Nat.Ioc_filter_dvd_card_eq_div, Nat.Ioc_filter_dvd_card_eq_div, Nat.cast_sub (Nat.div_le_div_right hab)] private def sieveDensity (S : Finset ℕ) : ℚ := ∏ p ∈ S, (1 - 1 / (p : ℚ)) private theorem sieve_density_expansion (S : Finset ℕ) : sieveDensity S = ∑ T ∈ S.powerset, (-1 : ℚ) ^ T.card / (∏ p ∈ T, p : ℕ) := by rw [sieveDensity, Finset.prod_sub] simp [div_eq_mul_inv] private theorem sieve_count_expansion (S : Finset ℕ) {a b : ℕ} (hab : a ≤ b) (hS : ∀ p ∈ S, Nat.Prime p) : (∑ x ∈ Ioc a b, (if Avoids S x then 1 else 0 : ℚ)) = ∑ T ∈ S.powerset, (-1 : ℚ) ^ T.card * ((b / (∏ p ∈ T, p) : ℕ) - (a / (∏ p ∈ T, p) : ℕ)) := by classical simp_rw [sieve_indicator S _ hS] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro T hT rw [← Finset.mul_sum] congr 1 calc (∑ x ∈ Ioc a b, (if (∏ p ∈ T, p) ∣ x then 1 else 0 : ℚ)) = (((Ioc a b).filter fun x ↦ (∏ p ∈ T, p) ∣ x).card : ℚ) := by simp _ = _ := multiples_count hab private theorem multiples_discrepancy {a b d : ℕ} (hab : a ≤ b) (hd : 0 < d) : |((b / d : ℕ) - (a / d : ℕ) : ℚ) - (b - a : ℕ) / (d : ℚ)| < 1 := by have hdQ : 0 < (d : ℚ) := by exact_mod_cast hd have hb : (b : ℚ) = (d : ℚ) * (b / d : ℕ) + (b % d : ℕ) := by exact_mod_cast (Nat.div_add_mod b d).symm have ha : (a : ℚ) = (d : ℚ) * (a / d : ℕ) + (a % d : ℕ) := by exact_mod_cast (Nat.div_add_mod a d).symm have hbr : (b % d : ℕ) < (d : ℚ) := by exact_mod_cast Nat.mod_lt b hd have har : (a % d : ℕ) < (d : ℚ) := by exact_mod_cast Nat.mod_lt a hd have hbr0 : (0 : ℚ) ≤ (b % d : ℕ) := by positivity have har0 : (0 : ℚ) ≤ (a % d : ℕ) := by positivity rw [Nat.cast_sub hab] have hquot : (((b : ℚ) - a) / d) * d = (b : ℚ) - a := div_mul_cancel₀ _ hdQ.ne' rw [abs_lt] constructor <;> nlinarith private theorem sieve_density_pos (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) : 0 < sieveDensity S := by apply Finset.prod_pos intro p hp have hp2 : (1 : ℚ) < p := by exact_mod_cast (hS p hp).one_lt have hinv : 1 / (p : ℚ) < 1 := (div_lt_one (by linarith)).mpr hp2 linarith /-- Distinct primes have density at least the reciprocal of their count plus one. -/ private theorem sieve_density_lower (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) : 1 ≤ (S.card + 1 : ℚ) * sieveDensity S := by induction S using Finset.induction_on_max with | empty => simp [sieveDensity] | @insert p S hmax ih => have hpS : p ∉ S := fun hp ↦ (hmax p hp).false have hp : Nat.Prime p := hS p (by simp) have hS' : ∀ q ∈ S, Nat.Prime q := fun q hq ↦ hS q (by simp [hq]) have hsub : S ⊆ Ico 2 p := by intro q hq exact Finset.mem_Ico.mpr ⟨(hS' q hq).two_le, hmax q hq⟩ have hcard : S.card + 2 ≤ p := by have hc := Finset.card_le_card hsub simp only [Nat.card_Ico] at hc have := hp.two_le omega have hcQ : (S.card : ℚ) + 2 ≤ p := by exact_mod_cast hcard have hpQ : (0 : ℚ) < p := by exact_mod_cast hp.pos have hfactor : (S.card : ℚ) + 1 ≤ ((S.card : ℚ) + 2) * (1 - 1 / (p : ℚ)) := by apply (mul_le_mul_iff_of_pos_right hpQ).mp field_simp nlinarith have hd := sieve_density_pos S hS' have hi := ih hS' have hmul := mul_le_mul_of_nonneg_right hfactor hd.le simp only [Finset.card_insert_of_notMem hpS, Nat.cast_add, Nat.cast_one] rw [sieveDensity, Finset.prod_insert hpS] change 1 ≤ ((S.card : ℚ) + 1 + 1) * ((1 - 1 / (p : ℚ)) * sieveDensity S) nlinarith private theorem sieve_count_discrepancy (S : Finset ℕ) {a b : ℕ} (hab : a ≤ b) (hS : ∀ p ∈ S, Nat.Prime p) : |(∑ x ∈ Ioc a b, (if Avoids S x then 1 else 0 : ℚ)) - (b - a : ℕ) * sieveDensity S| < (2 : ℚ) ^ S.card := by classical have heq : (∑ x ∈ Ioc a b, (if Avoids S x then 1 else 0 : ℚ)) - (b - a : ℕ) * sieveDensity S = ∑ T ∈ S.powerset, (-1 : ℚ) ^ T.card * (((b / (∏ p ∈ T, p) : ℕ) - (a / (∏ p ∈ T, p) : ℕ)) - (b - a : ℕ) / (∏ p ∈ T, p : ℕ)) := by rw [sieve_count_expansion S hab hS, sieve_density_expansion, Finset.mul_sum, ← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro T hT ring have hterm : ∀ T ∈ S.powerset, |(-1 : ℚ) ^ T.card * (((b / (∏ p ∈ T, p) : ℕ) - (a / (∏ p ∈ T, p) : ℕ)) - (b - a : ℕ) / (∏ p ∈ T, p : ℕ))| < 1 := by intro T hT have hTS : T ⊆ S := Finset.mem_powerset.mp hT have hd : 0 < ∏ p ∈ T, p := Finset.prod_pos (fun p hp ↦ (hS p (hTS hp)).pos) simpa only [abs_mul, abs_pow, abs_neg, abs_one, one_pow, one_mul] using multiples_discrepancy hab hd rw [heq] calc _ ≤ ∑ T ∈ S.powerset, |(-1 : ℚ) ^ T.card * (((b / (∏ p ∈ T, p) : ℕ) - (a / (∏ p ∈ T, p) : ℕ)) - (b - a : ℕ) / (∏ p ∈ T, p : ℕ))| := Finset.abs_sum_le_sum_abs _ _ _ < ∑ _T ∈ S.powerset, (1 : ℚ) := by apply Finset.sum_lt_sum (fun T hT ↦ (hterm T hT).le) exact ⟨∅, by simp, hterm ∅ (by simp)⟩ _ = (2 : ℚ) ^ S.card := by simp /-- Every interval of `(card(S)+1)*2^card(S)` consecutive positive integers contains one divisible by none of the distinct primes in `S`. -/ theorem prime_set_gap_bound (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) (a : ℕ) : ∃ x : ℕ, a < x ∧ x ≤ a + (S.card + 1) * 2 ^ S.card ∧ ∀ p ∈ S, ¬p ∣ x := by classical let J := (S.card + 1) * 2 ^ S.card have hdisc := sieve_count_discrepancy S (a := a) (b := a + J) (by omega) hS have hden := sieve_density_lower S hS have hJ : (J : ℚ) = ((S.card : ℚ) + 1) * (2 : ℚ) ^ S.card := by dsimp [J] push_cast rfl have hpow : (0 : ℚ) < 2 ^ S.card := by positivity have hmain : (2 : ℚ) ^ S.card ≤ J * sieveDensity S := by have hh := mul_le_mul_of_nonneg_right hden hpow.le rw [hJ] nlinarith have hcount : 0 < ∑ x ∈ Ioc a (a + J), (if Avoids S x then 1 else 0 : ℚ) := by simp only [Nat.add_sub_cancel_left] at hdisc have hlow := (abs_lt.mp hdisc).1 linarith by_contra hnot push Not at hnot have hzero : (∑ x ∈ Ioc a (a + J), (if Avoids S x then 1 else 0 : ℚ)) = 0 := by apply Finset.sum_eq_zero intro x hx obtain ⟨hax, hxa⟩ := Finset.mem_Ioc.mp hx have hav : ¬ Avoids S x := by intro h obtain ⟨p, hp, hpx⟩ := hnot x hax hxa exact h p hp hpx simp [hav] linarith /-- A fully elementary alternative to Kanold's sharper bound. -/ theorem elementary_coprime_gap_bound {r : ℕ} (hr : 0 < r) : HasCoprimeGaps r ((r.primeFactors.card + 1) * 2 ^ r.primeFactors.card) := by classical intro a by_cases hr1 : r = 1 · subst r exact ⟨a, le_rfl, by simp, by simp⟩ have hnonempty : r.primeFactors.Nonempty := by simp only [Finset.nonempty_iff_ne_empty, ne_eq, Nat.primeFactors_eq_empty] omega have hcard : 1 ≤ r.primeFactors.card := Finset.card_pos.mpr hnonempty have hJ : 2 ≤ (r.primeFactors.card + 1) * 2 ^ r.primeFactors.card := by have hp : 1 ≤ 2 ^ r.primeFactors.card := Nat.one_le_pow _ _ (by omega) nlinarith by_cases ha : a = 0 · subst a exact ⟨1, by omega, by omega, by simp⟩ obtain ⟨x, hxlo, hxhi, hxavoid⟩ := prime_set_gap_bound r.primeFactors (fun p hp ↦ Nat.prime_of_mem_primeFactors hp) (a - 1) refine ⟨x, by omega, by omega, ?_⟩ apply Nat.coprime_of_dvd intro p hp hpx hpr have hpmem : p ∈ r.primeFactors := Nat.mem_primeFactors.mpr ⟨hp, hpr, hr.ne'⟩ exact hxavoid p hpmem hpx end Bounty.CoprimeGaps end /- Proof component: FinitePatterns120 -/ section namespace Bounty.FiniteArithmetic120 open Math15.LonelyRunner Bounty.Arithmetic Bounty.FiniteArithmetic theorem deficit_le_six {s b:ℕ} (hs:0 omega theorem finite_faster_patterns120 {n s k:ℕ} (hn:3≤n) (hnbound:n≤120000) (hs:0 prime_divides_of_window hwindow hp hlo hhi have h2 : 2∣s := gcdWindow_prime_support hsn hwindow (by norm_num) (by omega) have h3 : 3∣s := gcdWindow_prime_support hsn hwindow (by norm_num) hk have hsbound : s<120000 := by omega have hb6 : b≤6 := deficit_le_six hs hsbound hbsmall (by dsimp [b]; omega) h2 h3 (fun p hp hlo hhi => hprime p hp hlo (hhi.trans_le (Nat.mul_le_mul_right b hk))) have hend : k*b≤19 := window_endpoint_le_nineteen hs hsbound hb6 h2 h3 hprime have hend5 : b≤5 → k*b≤17 := fun hb => window_endpoint_le_seventeen hs hsbound hb h2 h3 hprime have h6 : 6∣s := (by norm_num : Nat.Coprime 2 3).mul_dvd_of_dvd_of_dvd h2 h3 have h30 : b≤5 → 30∣s := by intro hb exact (by norm_num : Nat.Coprime 6 5).mul_dvd_of_dvd_of_dvd h6 (hprime 5 (by norm_num) hb (by nlinarith)) have h210 : b≤5 → 7 simp [hb,hh])⟩) · exact Or.inr (Or.inr (Or.inl ⟨hb,hke,h2310 (by omega) (by simp [hb,hke])⟩)) · exact Or.inr (Or.inr (Or.inr (Or.inl ⟨hb,hke,h30030 (by omega) (by rcases hke with hh | hh <;> simp [hb,hh])⟩))) · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨hb,hke,h210 (by omega) (by simp [hb,hke])⟩)))) · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨hb,hke,h2310 (by omega) (by simp [hb,hke])⟩))))) · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨hb,hke,h30030 (by omega) (by simp [hb,hke])⟩)))))) · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨hb,hke,h2310 (by omega) (by simp [hb,hke])⟩))))))) · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨hb,hke,h30030 (by omega) (by simp [hb,hke])⟩)))))))) · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨hb,hke,h30030 (by omega) (by simp [hb,hke])⟩))))))))) · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (⟨hb,hke,h102102 hb hke⟩)))))))))) end Bounty.FiniteArithmetic120 end /- Proof component: PrimeLadder -/ section namespace Bounty.PrimeLadder theorem prime_0 : Nat.Prime 31 := by norm_num theorem prime_1 : Nat.Prime 37 := by norm_num theorem prime_2 : Nat.Prime 43 := by norm_num theorem prime_3 : Nat.Prime 53 := by norm_num theorem prime_4 : Nat.Prime 61 := by norm_num theorem prime_5 : Nat.Prime 73 := by norm_num theorem prime_6 : Nat.Prime 89 := by norm_num theorem prime_7 : Nat.Prime 109 := by norm_num theorem prime_8 : Nat.Prime 131 := by norm_num theorem prime_9 : Nat.Prime 163 := by norm_num theorem prime_10 : Nat.Prime 199 := by norm_num theorem prime_11 : Nat.Prime 241 := by norm_num theorem prime_12 : Nat.Prime 293 := by norm_num theorem prime_13 : Nat.Prime 359 := by norm_num theorem prime_14 : Nat.Prime 443 := by norm_num theorem prime_15 : Nat.Prime 547 := by norm_num theorem prime_16 : Nat.Prime 683 := by norm_num theorem prime_17 : Nat.Prime 853 := by norm_num theorem prime_18 : Nat.Prime 1063 := by norm_num theorem prime_19 : Nat.Prime 1327 := by norm_num theorem prime_20 : Nat.Prime 1657 := by norm_num theorem prime_21 : Nat.Prime 2069 := by norm_num theorem prime_22 : Nat.Prime 2579 := by norm_num theorem prime_23 : Nat.Prime 3221 := by norm_num theorem prime_24 : Nat.Prime 4021 := by norm_num theorem prime_25 : Nat.Prime 5023 := by norm_num theorem prime_26 : Nat.Prime 6277 := by norm_num theorem prime_27 : Nat.Prime 7841 := by norm_num theorem prime_28 : Nat.Prime 9791 := by norm_num theorem prime_29 : Nat.Prime 12227 := by norm_num theorem prime_30 : Nat.Prime 15277 := by norm_num theorem prime_31 : Nat.Prime 19087 := by norm_num theorem prime_32 : Nat.Prime 23857 := by norm_num theorem prime_33 : Nat.Prime 29819 := by norm_num theorem prime_34 : Nat.Prime 37273 := by norm_num theorem prime_35 : Nat.Prime 46591 := by norm_num theorem prime_36 : Nat.Prime 58237 := by norm_num theorem prime_37 : Nat.Prime 72767 := by norm_num theorem prime_38 : Nat.Prime 90947 := by norm_num theorem prime_39 : Nat.Prime 113683 := by norm_num theorem prime_40 : Nat.Prime 142099 := by norm_num theorem prime_41 : Nat.Prime 177623 := by norm_num theorem prime_42 : Nat.Prime 222023 := by norm_num theorem prime_43 : Nat.Prime 277513 := by norm_num theorem prime_44 : Nat.Prime 346891 := by norm_num theorem prime_45 : Nat.Prime 433607 := by norm_num theorem prime_46 : Nat.Prime 541999 := by norm_num theorem prime_47 : Nat.Prime 677473 := by norm_num theorem prime_48 : Nat.Prime 846841 := by norm_num theorem prime_49 : Nat.Prime 1058549 := by norm_num theorem prime_50 : Nat.Prime 1323169 := by norm_num theorem prime_51 : Nat.Prime 1653959 := by norm_num theorem prime_52 : Nat.Prime 2067437 := by norm_num theorem prime_53 : Nat.Prime 2584291 := by norm_num theorem prime_54 : Nat.Prime 3230363 := by norm_num theorem prime_55 : Nat.Prime 4037953 := by norm_num theorem prime_56 : Nat.Prime 5047423 := by norm_num theorem prime_57 : Nat.Prime 6309271 := by norm_num theorem prime_58 : Nat.Prime 7886533 := by norm_num theorem prime_59 : Nat.Prime 9858157 := by norm_num theorem prime_60 : Nat.Prime 12322691 := by norm_num theorem prime_61 : Nat.Prime 15403363 := by norm_num theorem prime_62 : Nat.Prime 19254203 := by norm_num theorem prime_63 : Nat.Prime 24067741 := by norm_num theorem prime_64 : Nat.Prime 30084673 := by norm_num theorem prime_65 : Nat.Prime 37605839 := by norm_num theorem prime_66 : Nat.Prime 47007287 := by norm_num theorem prime_67 : Nat.Prime 58759091 := by norm_num theorem prime_68 : Nat.Prime 73448833 := by norm_num theorem prime_69 : Nat.Prime 91811017 := by norm_num theorem prime_70 : Nat.Prime 114763769 := by norm_num theorem quarter_interval_below_limit {y:ℕ} (hy:26≤y) (hymax:y<100000000) : ∃p:ℕ,Nat.Prime p ∧ y

hcong x hxlo (hxhi.trans_le htwom) hxcop) · have h2r := coprime_prime_of_boundary_gcd (by norm_num : Nat.Prime 2) h2B (by norm_num : ¬ 2 ∣ 3) hgcd have h5r := coprime_prime_of_boundary_gcd (by norm_num : Nat.Prime 5) h5B (by norm_num : ¬ 5 ∣ 3) hgcd have ha := displacement_three_deficit_lt har h2r h5r (fun x hxlo hxhi hxcop => hcong x hxlo (hxhi.trans_le htwom) hxcop) omega /-- A divisor of the other speed coprime to the displacement is coprime to this removed speed. -/ theorem coprime_of_dvd_boundary_gcd {c D B r : ℕ} (hcD : Nat.Coprime c D) (hcB : c ∣ B) (hgcd : Nat.gcd D r = Nat.gcd B r) : Nat.Coprime c r := by have hgr : Nat.gcd c r ∣ Nat.gcd B r := Nat.dvd_gcd ((Nat.gcd_dvd_left c r).trans hcB) (Nat.gcd_dvd_right c r) rw [← hgcd] at hgr have hgD : Nat.gcd c r ∣ D := hgr.trans (Nat.gcd_dvd_left D r) have hone : Nat.gcd c r ∣ 1 := by rw [← hcD.gcd_eq_one] exact Nat.dvd_gcd (Nat.gcd_dvd_left c r) hgD exact Nat.dvd_one.mp hone /-- A necessary gcd constraint on the two small deficits. -/ theorem deficit_gcd_dvd_displacement {n r s a b k D M : ℕ} (hna : n = r + a) (hnb : n = s + b) (hba : b ≤ a) (hMs : M ∣ s) (hgcd : Nat.gcd D r = Nat.gcd (k * s) r) : Nat.gcd M (a-b) ∣ D := by have hgs : Nat.gcd M (a-b) ∣ s := (Nat.gcd_dvd_left M (a-b)).trans hMs have hgr : Nat.gcd M (a-b) ∣ r := by have hh := Nat.dvd_sub hgs (Nat.gcd_dvd_right M (a-b)) have heq : s - (a-b) = r := by omega rwa [heq] at hh have hgB : Nat.gcd M (a-b) ∣ k*s := dvd_mul_of_dvd_right hgs k have hgd := Nat.dvd_gcd hgB hgr rw [← hgcd] at hgd exact hgd.trans (Nat.gcd_dvd_left D r) theorem mem_range_one {x a n : ℕ} : x ∈ List.range' a n ↔ a ≤ x ∧ x < a+n := by rw [List.mem_range'] constructor · rintro ⟨i, hi, rfl⟩ omega · rintro ⟨hlo, hhi⟩ exact ⟨x-a, by omega, by omega⟩ /-- A small, fully checked certificate either violates a necessary gcd or provides a smooth unit incompatible with the unwrapped residue equation. -/ def tupleCertified (a b k m D M : ℕ) : Bool := if m + k ≤ m * D then true else if b ≤ a ∧ ¬ Nat.gcd M (a-b) ∣ D then true else (List.range' a ((m-1)*a)).any (fun x => decide (x ∣ (M / Nat.gcd M D)^10 ∧ D*x+k*b ≠ k*a)) def smallTupleTable (b k M bound : ℕ) : Bool := (List.range' 1 (bound-1)).all (fun a => (List.range' 2 (k-2)).all (fun m => (List.range' 2 3).all (fun D => tupleCertified a b k m D M))) theorem tupleCertified_witness {a b k m D M : ℕ} (hm : 2 ≤ m) (hbound : m*D < m+k) (hgd : b ≤ a → Nat.gcd M (a-b) ∣ D) (hcert : tupleCertified a b k m D M = true) : ∃ x : ℕ, a ≤ x ∧ x < m*a ∧ x ∣ (M / Nat.gcd M D)^10 ∧ D*x+k*b ≠ k*a := by have hnbad : ¬ (b ≤ a ∧ ¬ Nat.gcd M (a-b) ∣ D) := by tauto simp only [tupleCertified, ite_eq_right (not_le_of_gt hbound), ite_eq_right hnbad, List.any_eq_true] at hcert obtain ⟨x, hxmem, hx⟩ := hcert have hxr := mem_range_one.mp hxmem have hcheck : x ∣ (M / Nat.gcd M D)^10 ∧ D*x+k*b ≠ k*a := of_decide_eq_true hx refine ⟨x, hxr.1, ?_, hcheck.1, hcheck.2⟩ have heq : a + (m-1)*a = m*a := by nlinarith [Nat.sub_add_cancel (show 1 ≤ m by omega)] simpa only [heq] using hxr.2 theorem smallTupleTable_entry {a b k m D M bound : ℕ} (ha : 0 < a) (hab : a < bound) (hm : 2 ≤ m) (hmk : m < k) (hD : 2 ≤ D) (hD4 : D ≤ 4) (ht : smallTupleTable b k M bound = true) : tupleCertified a b k m D M = true := by simp only [smallTupleTable, List.all_eq_true] at ht exact ht a (mem_range_one.mpr ⟨by omega, by omega⟩) m (mem_range_one.mpr ⟨hm, by omega⟩) D (mem_range_one.mpr ⟨hD, by omega⟩) /-- A verified small tuple rules out a large modulus by unwrapping its common residue, using only smoothness certificates and exact integer arithmetic. -/ theorem large_modulus_tuple_obstruction {n r s a b k m D M : ℕ} (hna : n = r+a) (hnb : n = s+b) (hm : 2 ≤ m) (hD : 0 < D) (hbound : m*D < m+k) (hMs : M ∣ s) (hbase : Nat.Coprime (M / Nat.gcd M D) D) (hgcd : Nat.gcd D r = Nat.gcd (k*s) r) (hsize : D*(m*a)+k*b ≤ r) (hka : k*a < r) (hcong : ∀ x : ℕ, a ≤ x → x < m*a → Nat.Coprime x r → Nat.ModEq r (D*x) (k*s)) (hcert : tupleCertified a b k m D M = true) : False := by have hgd : b ≤ a → Nat.gcd M (a-b) ∣ D := fun hba => deficit_gcd_dvd_displacement hna hnb hba hMs hgcd obtain ⟨x, hxlo, hxhi, hxdiv, hxne⟩ := tupleCertified_witness hm hbound hgd hcert have hbaseM : M / Nat.gcd M D ∣ M := Nat.div_dvd_of_dvd (Nat.gcd_dvd_left M D) have hbaseB : M / Nat.gcd M D ∣ k*s := dvd_mul_of_dvd_right (hbaseM.trans hMs) k have hbaser := coprime_of_dvd_boundary_gcd hbase hbaseB hgcd have hxr : Nat.Coprime x r := (hbaser.pow_left 10).of_dvd_left hxdiv have hmod := Nat.ModEq.add_right (k*b) (hcong x hxlo hxhi hxr) have hright : (k*s+k*b) % r = (k*a) % r := by have heq : k*s+k*b = k*r+k*a := by nlinarith [hna, hnb] rw [heq] simp change (D*x+k*b)%r = (k*s+k*b)%r at hmod rw [hright] at hmod have hsmall : D*x+k*b < r := by have hmul := Nat.mul_lt_mul_of_pos_left hxhi hD omega rw [Nat.mod_eq_of_lt hsmall, Nat.mod_eq_of_lt hka] at hmod exact hxne hmod theorem table_2_3_30 : smallTupleTable 2 3 30 75 = true := by decide +kernel theorem table_2_4_210 : smallTupleTable 2 4 210 75 = true := by decide +kernel theorem table_2_5_210 : smallTupleTable 2 5 210 75 = true := by decide +kernel theorem table_2_6_2310 : smallTupleTable 2 6 2310 75 = true := by decide +kernel theorem table_2_7_30030 : smallTupleTable 2 7 30030 75 = true := by decide +kernel theorem table_2_8_30030 : smallTupleTable 2 8 30030 75 = true := by decide +kernel theorem table_3_3_210 : smallTupleTable 3 3 210 75 = true := by decide +kernel theorem table_3_4_2310 : smallTupleTable 3 4 2310 75 = true := by decide +kernel theorem table_3_5_30030 : smallTupleTable 3 5 30030 75 = true := by decide +kernel theorem table_4_3_2310 : smallTupleTable 4 3 2310 75 = true := by decide +kernel theorem table_4_4_30030 : smallTupleTable 4 4 30030 75 = true := by decide +kernel theorem table_5_3_30030 : smallTupleTable 5 3 30030 75 = true := by decide +kernel theorem table_6_3_102102 : smallTupleTable 6 3 102102 343 = true := by decide +kernel /-- Candidate units used by the small-modulus certificate. -/ def finiteCandidates (n r m : ℕ) : List ℕ := List.range' (n-r) (min (m*(n-r)) n - (n-r)) def structuralFailure (n r s m k D : ℕ) : Prop := r = s ∨ Nat.gcd r s ≤ 1 ∨ (k*s)%r=0 ∨ (m*r)%s=0 ∨ k*s ≤ m*r ∨ m+k ≤ m*D ∨ k*s+m*r < n*m*D ∨ n*m*D+m*r < k*s ∨ Nat.gcd D r ≠ Nat.gcd (k*s) r def structuralFailureDecidable (n r s m k D : ℕ) : Decidable (structuralFailure n r s m k D) := inferInstanceAs (Decidable (_ ∨ _ ∨ _ ∨ _ ∨ _ ∨ _ ∨ _ ∨ _ ∨ _)) def smallConfig (n r s m k D : ℕ) : Bool := letI := structuralFailureDecidable n r s m k D if structuralFailure n r s m k D then true else let xs := finiteCandidates n r m xs.all (fun x => decide (Nat.gcd r x ≠ 1)) || xs.any (fun x => decide (Nat.gcd r x = 1 ∧ (D*x)%r ≠ (k*s)%r)) def smallRow (b s k : ℕ) : Bool := let n := s+b (List.range' 1 74).all (fun a => let r := n-a if n-1 < 2*r ∧ 0 (List.range' 2 3).all (fun D => smallConfig n r s m k D)) else true) def smallRows (b k M count : ℕ) : Bool := (List.range' 1 count).all (fun j => smallRow b (M*j) k) theorem small_rows_2_3_30 : smallRows 2 3 30 135 = true := by decide +kernel theorem small_rows_2_4_210 : smallRows 2 4 210 19 = true := by decide +kernel theorem small_rows_2_5_210 : smallRows 2 5 210 19 = true := by decide +kernel theorem small_rows_2_6_2310 : smallRows 2 6 2310 1 = true := by decide +kernel theorem small_rows_3_3_210 : smallRows 3 3 210 19 = true := by decide +kernel theorem small_rows_3_4_2310 : smallRows 3 4 2310 1 = true := by decide +kernel theorem small_rows_4_3_2310 : smallRows 4 3 2310 1 = true := by decide +kernel theorem smallConfig_obstruction {n r s m k D : ℕ} (hnot : ¬ structuralFailure n r s m k D) (hunit : ∃ x : ℕ, n-r ≤ x ∧ x < m*(n-r) ∧ x omega have hD4:D≤4 := by nlinarith have har:n-r≤r := by omega have hcong2:∀x:ℕ,n-r≤x → x<2*(n-r) → Nat.Coprime x r → Nat.ModEq r (D*x) (k*s) := by intro x hxlo hxhi hxcop exact hcong x hxlo (hxhi.trans_le (Nat.mul_le_mul_right (n-r) hm)) hxcop have hunit:∃x:ℕ,n-r≤x ∧ xha75) hcount hbase hgcd hbound (by nlinarith) (by nlinarith) hnot hunit hcong ht htsmall -- Each following branch is one exact faster-acceleration pattern. rcases hcases with ⟨hb,hk,hM⟩|⟨hb,hk,hM⟩|⟨hb,hk,hM⟩|⟨hb,hk,hM⟩|⟨hb,hk,hM⟩|⟨hb,hk,hM⟩|⟨hb,hk,hM⟩|⟨hb,hk,hM⟩|⟨hb,hk,hM⟩|⟨hb,hk,hM⟩|⟨hb,hk,hM⟩ · subst k exact normal_pattern 2 30 135 (by norm_num) (by omega) hM (by norm_num) (by norm_num) (by norm_num) (by interval_cases D <;> norm_num) table_2_3_30 small_rows_2_3_30 · rcases hk with rfl | rfl · exact normal_pattern 2 210 19 (by norm_num) (by omega) hM (by norm_num) (by norm_num) (by norm_num) (by interval_cases D <;> norm_num) table_2_4_210 small_rows_2_4_210 · exact normal_pattern 2 210 19 (by norm_num) (by omega) hM (by norm_num) (by norm_num) (by norm_num) (by interval_cases D <;> norm_num) table_2_5_210 small_rows_2_5_210 · subst k exact normal_pattern 2 2310 1 (by norm_num) (by omega) hM (by norm_num) (by norm_num) (by norm_num) (by interval_cases D <;> norm_num) table_2_6_2310 small_rows_2_6_2310 · rcases hk with rfl | rfl · exact normal_pattern 2 30030 0 (by norm_num) (by omega) hM (by norm_num) (by norm_num) (by norm_num) (by interval_cases D <;> norm_num) table_2_7_30030 (by rfl) · exact normal_pattern 2 30030 0 (by norm_num) (by omega) hM (by norm_num) (by norm_num) (by norm_num) (by interval_cases D <;> norm_num) table_2_8_30030 (by rfl) · subst k exact normal_pattern 3 210 19 (by norm_num) (by omega) hM (by norm_num) (by norm_num) (by norm_num) (by interval_cases D <;> norm_num) table_3_3_210 small_rows_3_3_210 · subst k exact normal_pattern 3 2310 1 (by norm_num) (by omega) hM (by norm_num) (by norm_num) (by norm_num) (by interval_cases D <;> norm_num) table_3_4_2310 small_rows_3_4_2310 · subst k exact normal_pattern 3 30030 0 (by norm_num) (by omega) hM (by norm_num) (by norm_num) (by norm_num) (by interval_cases D <;> norm_num) table_3_5_30030 (by rfl) · subst k exact normal_pattern 4 2310 1 (by norm_num) (by omega) hM (by norm_num) (by norm_num) (by norm_num) (by interval_cases D <;> norm_num) table_4_3_2310 small_rows_4_3_2310 · subst k exact normal_pattern 4 30030 0 (by norm_num) (by omega) hM (by norm_num) (by norm_num) (by norm_num) (by interval_cases D <;> norm_num) table_4_4_30030 (by rfl) · subst k exact normal_pattern 5 30030 0 (by norm_num) (by omega) hM (by norm_num) (by norm_num) (by norm_num) (by interval_cases D <;> norm_num) table_5_3_30030 (by rfl) · subst k have hm2:m=2 := by omega subst m have hD2:D=2 := by omega subst D have h3B:3∣3*s:=dvd_mul_of_dvd_right ((by norm_num:3∣102102).trans hM) 3 have h7B:7∣3*s:=dvd_mul_of_dvd_right ((by norm_num:7∣102102).trans hM) 3 have h11B:11∣3*s:=dvd_mul_of_dvd_right ((by norm_num:11∣102102).trans hM) 3 have ha343:=displacement_two_seven_eleven_deficit_lt har (coprime_prime_of_boundary_gcd (by norm_num) h3B (by norm_num) hgcd) (coprime_prime_of_boundary_gcd (by norm_num) h7B (by norm_num) hgcd) (coprime_prime_of_boundary_gcd (by norm_num) h11B (by norm_num) hgcd) hcong2 have hsmall:r<4000 → n-r<75 := by intro hrsmall have hslarge:=Nat.le_of_dvd hs hM omega exact pattern_obstruction (count := 0) hr hs hrn hupperr hm hmk hD hD4 (by omega : n=s+6) hM (by norm_num) ha343 hsmall (by norm_num) (by norm_num) hgcd hbound (by omega) (by omega) hnot hunit hcong table_6_3_102102 (by rfl) end Bounty.FiniteRejection end /- Proof component: VonMangoldtCompatibility -/ section /- Adapted from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt, Copyright (c) 2022 Bhavik Mehta, licensed under Apache 2.0. -/ namespace ArithmeticFunction open Finset Nat open scoped ArithmeticFunction noncomputable def log : ArithmeticFunction ℝ := ⟨fun n => Real.log n, by simp⟩ theorem log_apply {n : ℕ} : log n = Real.log n := rfl noncomputable def vonMangoldt : ArithmeticFunction ℝ := ⟨fun n => if IsPrimePow n then Real.log (minFac n) else 0, ite_eq_right not_isPrimePow_zero⟩ theorem vonMangoldt_apply {n : ℕ} : vonMangoldt n = if IsPrimePow n then Real.log (minFac n) else 0 := rfl theorem vonMangoldt_apply_one : vonMangoldt 1 = 0 := by simp [vonMangoldt_apply] theorem vonMangoldt_nonneg {n : ℕ} : 0 ≤ vonMangoldt n := by rw [vonMangoldt_apply] split_ifs · exact Real.log_nonneg (one_le_cast.2 (Nat.minFac_pos n)) rfl theorem vonMangoldt_apply_pow {n k : ℕ} (hk : k ≠ 0) : vonMangoldt (n ^ k) = vonMangoldt n := by simp only [vonMangoldt_apply, isPrimePow_pow_iff hk, pow_minFac hk] theorem vonMangoldt_apply_prime {p : ℕ} (hp : p.Prime) : vonMangoldt p = Real.log p := by rw [vonMangoldt_apply, Prime.minFac_eq hp, ite_eq_left hp.prime.isPrimePow] theorem vonMangoldt_ne_zero_iff {n : ℕ} : vonMangoldt n ≠ 0 ↔ IsPrimePow n := by rcases eq_or_ne n 1 with (rfl | hn) · simp [vonMangoldt_apply_one, not_isPrimePow_one] exact (Real.log_pos (one_lt_cast.2 (minFac_prime hn).one_lt)).ne'.ite_ne_right_iff theorem vonMangoldt_pos_iff {n : ℕ} : 0 < vonMangoldt n ↔ IsPrimePow n := vonMangoldt_nonneg.lt_iff_ne.trans (ne_comm.trans vonMangoldt_ne_zero_iff) theorem vonMangoldt_eq_zero_iff {n : ℕ} : vonMangoldt n = 0 ↔ ¬IsPrimePow n := vonMangoldt_ne_zero_iff.not_right theorem vonMangoldt_sum {n : ℕ} : ∑ i ∈ n.divisors, vonMangoldt i = Real.log n := by refine recOnPrimeCoprime ?_ ?_ ?_ n · simp · intro p k hp rw [sum_divisors_prime_pow hp, cast_pow, Real.log_pow, Finset.sum_range_succ', Nat.pow_zero, vonMangoldt_apply_one] simp [vonMangoldt_apply_pow (Nat.succ_ne_zero _), vonMangoldt_apply_prime hp] intro a b ha' hb' hab ha hb simp only [vonMangoldt_apply, ← sum_filter] at ha hb ⊢ rw [mul_divisors_filter_prime_pow hab, filter_union, sum_union (disjoint_divisors_filter_isPrimePow hab), ha, hb, Nat.cast_mul, Real.log_mul (cast_ne_zero.2 (pos_of_gt ha').ne') (cast_ne_zero.2 (pos_of_gt hb').ne')] open scoped zeta theorem vonMangoldt_mul_zeta : vonMangoldt * ζ = log := by ext n rw [coe_mul_zeta_apply, vonMangoldt_sum] rfl theorem vonMangoldt_le_log : ∀ {n : ℕ}, vonMangoldt n ≤ Real.log (n : ℝ) | 0 => by simp | n + 1 => by rw [← vonMangoldt_sum] exact single_le_sum (by exact fun _ _ => vonMangoldt_nonneg) (mem_divisors_self _ n.succ_ne_zero) end ArithmeticFunction /- Adapted from Mathlib.Algebra.Order.Floor.Semifield, Copyright (c) 2018 Mario Carneiro, authors Mario Carneiro and Kevin Kappelmann, licensed under Apache 2.0. -/ theorem Nat.floor_div_natCast {K : Type*} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (a : K) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n := by obtain rfl | hn := n.eq_zero_or_pos · simp nth_rw 2 [← div_mul_cancel₀ (a := a) (b := ↑n) (by positivity)] rw [Nat.mul_cast_floor_div_cancel (Nat.ne_zero_of_lt hn)] end /- Proof component: ChebyshevCompatibility -/ section /- Adapted from Mathlib.NumberTheory.Chebyshev, copyright (c) 2025 Alastair Irving. Authors: Alastair Irving, Terry Tao, Ruben Van de Velde. Licensed under Apache 2.0. Only finite sums and elementary real inequalities are used here. -/ open Nat hiding log open Finset Real open ArithmeticFunction hiding log id open scoped Nat.Prime namespace Chebyshev noncomputable def psi (x : ℝ) : ℝ := ∑ n ∈ Ioc 0 ⌊x⌋₊, ArithmeticFunction.vonMangoldt n /-- The sum of `log p` over primes `p ≤ x`. -/ noncomputable def theta (x : ℝ) : ℝ := ∑ p ∈ Ioc 0 ⌊x⌋₊ with p.Prime, log p theorem psi_nonneg (x : ℝ) : 0 ≤ psi x := sum_nonneg fun _ _ ↦ vonMangoldt_nonneg theorem theta_nonneg (x : ℝ) : 0 ≤ theta x := sum_nonneg fun _ _ ↦ log_nonneg (by aesop) theorem theta_pos {x : ℝ} (hy : 2 ≤ x) : 0 < theta x := by refine sum_pos (fun n hn ↦ log_pos ?_) ⟨2, ?_⟩ · simp only [mem_filter] at hn; exact_mod_cast hn.2.one_lt · have : 0 ≤ x := by grind simpa using ⟨(le_floor_iff this).2 hy, prime_two⟩ theorem psi_eq_sum_Icc (x : ℝ) : psi x = ∑ n ∈ Icc 0 ⌊x⌋₊, ArithmeticFunction.vonMangoldt n := by rw [psi, ← add_sum_Ioc_eq_sum_Icc] <;> simp theorem theta_eq_sum_Icc (x : ℝ) : theta x = ∑ p ∈ Icc 0 ⌊x⌋₊ with p.Prime, log p := by rw [theta, sum_filter, sum_filter, ← add_sum_Ioc_eq_sum_Icc] <;> simp theorem psi_eq_zero_of_lt_two {x : ℝ} (hx : x < 2) : psi x = 0 := by apply sum_eq_zero fun n hn ↦ ?_ simp only [mem_Ioc] at hn convert! vonMangoldt_apply_one have := lt_of_le_of_lt (le_floor_iff' hn.1.ne' |>.mp hn.2) hx norm_cast at this linarith theorem psi_eq_zero_iff {x : ℝ} : psi x = 0 ↔ x < 2 := by refine ⟨fun h₀ ↦ ?_, psi_eq_zero_of_lt_two⟩ by_contra! contra replace contra : 2 ∈ Ioc 0 ⌊x⌋₊ := by rw [mem_Ioc, le_floor_iff (by grind)]; grind have : ArithmeticFunction.vonMangoldt 2 ≤ psi x := single_le_sum (fun n _ ↦ vonMangoldt_nonneg (n := n)) contra have := vonMangoldt_pos_iff.mpr prime_two.isPrimePow linarith theorem psi_eq_zero_of_le_one {x : ℝ} (hx : x ≤ 1) : psi x = 0 := psi_eq_zero_of_lt_two (by linarith) theorem psi_zero : psi 0 = 0 := psi_eq_zero_of_lt_two zero_lt_two theorem psi_one : psi 1 = 0 := psi_eq_zero_of_lt_two one_lt_two theorem theta_eq_zero_of_lt_two {x : ℝ} (hx : x < 2) : theta x = 0 := by apply sum_eq_zero fun n hn ↦ ?_ convert! log_one simp only [mem_filter, mem_Ioc] at hn have := lt_of_le_of_lt (le_floor_iff' hn.1.1.ne' |>.mp hn.1.2) hx norm_cast at ⊢ this linarith theorem theta_eq_zero_iff {x : ℝ} : theta x = 0 ↔ x < 2 := by refine ⟨fun h₀ ↦ ?_, theta_eq_zero_of_lt_two⟩ by_contra! contra replace contra : 2 ∈ Ioc 0 ⌊x⌋₊ := by rw [mem_Ioc, le_floor_iff (by grind)]; grind have h₁ : log (↑(2 : ℕ) : ℝ) ≤ theta x := single_le_sum (fun p hp ↦ log_nonneg (by aesop)) (by aesop (add simp prime_two)) have := Real.log_pos one_lt_two grind theorem theta_eq_zero_of_le_one {x : ℝ} (hx : x ≤ 1) : theta x = 0 := theta_eq_zero_of_lt_two (by linarith) theorem theta_zero : theta 0 = 0 := theta_eq_zero_of_lt_two zero_lt_two theorem theta_one : theta 1 = 0 := theta_eq_zero_of_lt_two one_lt_two theorem psi_eq_psi_coe_floor (x : ℝ) : psi x = psi ⌊x⌋₊ := by unfold psi rw [floor_natCast] theorem theta_eq_theta_coe_floor (x : ℝ) : theta x = theta ⌊x⌋₊ := by unfold theta rw [floor_natCast] theorem psi_mono : Monotone psi := by intro x y hxy apply sum_le_sum_of_subset_of_nonneg · exact Ioc_subset_Ioc (by rfl) (by gcongr) · intro i _ _ exact vonMangoldt_nonneg theorem theta_mono : Monotone theta := by intro x y hxy apply sum_le_sum_of_subset_of_nonneg · exact filter_subset_filter _ <| Ioc_subset_Ioc_right (by gcongr) · exact fun p _ _ ↦ log_natCast_nonneg p /-- `theta x` is the log of the product of the primes up to `x`. -/ theorem theta_eq_log_primorial (x : ℝ) : theta x = log (primorial ⌊x⌋₊) := by unfold theta primorial rw [cast_prod, log_prod (fun p hp ↦ mod_cast (mem_filter.mp hp).2.pos.ne')] congr 1 with p simp_all [Prime.pos] /-- Chebyshev's upper bound: `theta x ≤ c x` with the constant `c = log 4`. -/ theorem theta_le_log4_mul_x {x : ℝ} (hx : 0 ≤ x) : theta x ≤ log 4 * x := by rw [theta_eq_log_primorial] trans log (4 ^ ⌊x⌋₊) · gcongr <;> norm_cast exacts [primorial_pos _, primorial_le_four_pow _] rw [Real.log_pow, mul_comm] gcongr exact floor_le hx theorem sum_PrimePow_eq_sum_sum' {R : Type*} [AddCommMonoid R] (f : ℕ → R) {x : ℝ} (hx : 0 ≤ x) {N : ℕ} (hN : ⌊log x / log 2⌋₊ ≤ N) : ∑ n ∈ Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n = ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ ((1 : ℝ) / k)⌋₊ with p.Prime, f (p ^ k) := by trans ∑ ⟨k, p⟩ ∈ Icc 1 N ×ˢ (Ioc 0 ⌊x⌋₊).filter Nat.Prime with p ≤ ⌊x ^ (k : ℝ)⁻¹⌋₊, f (p ^ k) · refine (sum_bij (i := fun ⟨k, p⟩ _ ↦ p ^ k) ?_ ?_ ?_ ?_).symm · simp +contextual [hx, rpow_nonneg, le_floor_iff, ← pos_iff_ne_zero, Prime.isPrimePow, one_le_iff_ne_zero, le_rpow_inv_iff_of_pos, isPrimePow_pow_iff, prime_iff] · simp +contextual only [hx, rpow_nonneg, le_floor_iff, mem_filter, mem_product, mem_Icc, one_le_iff_ne_zero, pos_iff_ne_zero, mem_Ioc, and_imp, Prod.forall, Prod.mk.injEq] intro k₁ p₁ hk₁ _ _ _ hp₁ _ k₂ p₂ hk₂ _ _ _ hp₂ _ H exact (hp₁.pow_inj' hp₂ hk₁ hk₂ H).symm · simp +contextual only [mem_filter, mem_Ioc, hx, le_floor_iff, and_assoc, rpow_nonneg, mem_product, mem_Icc, succ_le_iff, exists_prop, Prod.exists, exists_and_left, and_imp] rintro b _ hbx ⟨p, k, hp, hk₀, rfl⟩ rw [cast_pow] at hbx refine ⟨k, hk₀, (le_floor ?_).trans hN, p, hp.nat_prime.pos, ?_, hp.nat_prime, ?_, rfl⟩ · rw [le_div_iff₀ (log_pos (by norm_num)), ← Real.log_pow] gcongr apply (LE.le.trans ?_ hbx) exact pow_le_pow_left₀ (by norm_num) (mod_cast hp.nat_prime.two_le) _ · exact (le_self_pow₀ (mod_cast hp.nat_prime.one_le) hk₀.ne').trans hbx · simp_all [le_rpow_inv_iff_of_pos] · simp · rw [sum_filter, sum_product] refine sum_congr rfl fun k _ ↦ ?_ simp only [sum_ite, not_le, sum_const_zero, add_zero] congr 1 ext p simp only [mem_filter, mem_Ioc] refine ⟨fun _ ↦ (by simp_all), fun h ↦ ?_⟩ simp_all only [mem_Icc, one_div, true_and, and_true] grw [h.1.2, floor_le_floor] apply rpow_le_self_of_one_le _ (by bound) have := one_le_floor_iff _ |>.mp <| le_trans (one_le_cast.mp h.2.one_le) h.1.2 contrapose! this apply rpow_lt_one hx this (by bound) theorem sum_PrimePow_eq_sum_sum {R : Type*} [AddCommMonoid R] (f : ℕ → R) {x : ℝ} (hx : 0 ≤ x) : ∑ n ∈ Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n = ∑ k ∈ Icc 1 ⌊log x / log 2⌋₊, ∑ p ∈ Ioc 0 ⌊x ^ ((1 : ℝ) / k)⌋₊ with p.Prime, f (p ^ k) := sum_PrimePow_eq_sum_sum' f hx (le_refl _) theorem psi_eq_sum_theta' {x : ℝ} (hx : 0 ≤ x) {N : ℕ} (hN : ⌊log x / log 2⌋₊ ≤ N) : psi x = ∑ n ∈ Icc 1 N, theta (x ^ ((1 : ℝ) / n)) := by simp_rw [psi, vonMangoldt_apply, ← sum_filter, sum_PrimePow_eq_sum_sum' _ hx hN] apply sum_congr rfl fun _ hk ↦ sum_congr rfl fun _ _ ↦ ?_ rw [Prime.pow_minFac _ (by linarith [mem_Icc.mp hk])] simp_all theorem psi_eq_sum_theta {x : ℝ} (hx : 0 ≤ x) : psi x = ∑ n ∈ Icc 1 ⌊log x / log 2⌋₊, theta (x ^ ((1 : ℝ) / n)) := psi_eq_sum_theta' hx (le_refl _) theorem psi_eq_theta_add_sum_theta' {x : ℝ} (hx : 2 ≤ x) {N : ℕ} (hN : ⌊log x / log 2⌋₊ ≤ N) : psi x = theta x + ∑ n ∈ Icc 2 N, theta (x ^ ((1 : ℝ) / n)) := by rw [psi_eq_sum_theta' (by linarith) hN, ← add_sum_Ioc_eq_sum_Icc] · congr simp · apply le_trans _ hN rw [le_floor_iff' one_ne_zero, le_div_iff₀ (by positivity), cast_one, one_mul] gcongr theorem psi_eq_theta_add_sum_theta {x : ℝ} (hx : 2 ≤ x) : psi x = theta x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, theta (x ^ ((1 : ℝ) / n)) := psi_eq_theta_add_sum_theta' hx (le_refl _) theorem theta_le_psi (x : ℝ) : theta x ≤ psi x := by by_cases! h : x < 2 · rw [theta_eq_zero_of_lt_two h, psi_eq_zero_of_lt_two h] rw [psi_eq_theta_add_sum_theta h] simp only [le_add_iff_nonneg_right] exact sum_nonneg fun _ _ ↦ theta_nonneg _ /-- `|psi x - theta x| ≤ c √ x log x` with an explicit constant c. To remove the log, see `psi_sub_theta_le_mul_sqrt`. -/ theorem abs_psi_sub_theta_le_sqrt_mul_log {x : ℝ} (hx : 1 ≤ x) : |psi x - theta x| ≤ 2 * x.sqrt * x.log := by by_cases! hx : x < 2 · rw [psi_eq_zero_of_lt_two hx, theta_eq_zero_of_lt_two hx, sub_zero, abs_zero] bound rw [psi_eq_theta_add_sum_theta hx, add_sub_cancel_left] apply le_trans <| abs_sum_le_sum_abs .. simp_rw [abs_of_nonneg <| theta_nonneg _] trans ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * x.sqrt · gcongr with i hi apply le_trans (theta_le_log4_mul_x (rpow_nonneg (by linarith) _)) rw [sqrt_eq_rpow] gcongr; simp_all simp only [sum_const, card_Icc, reduceSubDiff, nsmul_eq_mul] calc _ ≤ (log x / log 2) * (log 4 * √x) := by gcongr rw [cast_sub] · trans ↑⌊log x / log 2⌋₊ · linarith · exact floor_le (by bound) apply le_floor norm_cast apply one_le_div _ |>.mpr <;> bound _ = (log 4 / log 2) * x.sqrt * x.log := by field _ = _ := by congr rw [(by norm_num : (4 : ℝ) = 2 ^ 2), Real.log_pow] field /-- Explicit upper bound on `psi`. -/ theorem psi_le {x : ℝ} (hx : 1 ≤ x) : psi x ≤ log 4 * x + 2 * x.sqrt * x.log := by calc _ = psi x - theta x + theta x := by ring _ ≤ 2 * x.sqrt * x.log + log 4 * x := by gcongr · exact le_trans (le_abs_self _) (abs_psi_sub_theta_le_sqrt_mul_log hx) · exact theta_le_log4_mul_x (by linarith) _ = _ := by ring /-- Chebyshev's bound `psi x ≤ c x` with an explicit constant. Note that `Chebyshev.psi_le` gives a sharper bound with a better main term. -/ theorem psi_le_const_mul_self {x : ℝ} (hx : 0 ≤ x) : psi x ≤ (log 4 + 4) * x := by by_cases! hx : x < 1 · rw [psi_eq_zero_of_lt_two (by linarith)] bound apply le_trans (psi_le hx) rw [add_mul] gcongr 1 grw [sqrt_eq_rpow, log_le_rpow_div (ε := 1 / 2) (by linarith) (by linarith), ← mul_div_assoc, ← mul_one_div] nth_rw 2 [mul_assoc] rw [← rpow_add (by linarith)] norm_num linarith theorem psi_sub_theta_le {x : ℝ} (hx : 1 ≤ x) : psi x - theta x ≤ 2 * √x * log x := by grw [← abs_psi_sub_theta_le_sqrt_mul_log hx] exact le_abs_self _ end Chebyshev end /- Proof component: LogSumBounds -/ section noncomputable section namespace Bounty.LogSum open Real Finset def F (x : ℝ) : ℝ := x * log x - x theorem difference_bounds {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : (y - x) * log x ≤ F y - F x ∧ F y - F x ≤ (y - x) * log y := by have h1 := Real.log_le_sub_one_of_pos (div_pos hx hy) have h2 := Real.log_le_sub_one_of_pos (div_pos hy hx) rw [Real.log_div hx.ne' hy.ne'] at h1 rw [Real.log_div hy.ne' hx.ne'] at h2 have h1m := mul_le_mul_of_nonneg_left h1 hy.le have h2m := mul_le_mul_of_nonneg_left h2 hx.le have e1 : y * (x / y - 1) = x - y := by field_simp have e2 : x * (y / x - 1) = y - x := by field_simp rw [e1] at h1m rw [e2] at h2m dsimp [F] constructor <;> nlinarith theorem nat_sum_bounds (n : ℕ) (hn : 1 ≤ n) : F n + 1 ≤ ∑ i ∈ Icc 1 n, log (i : ℝ) ∧ (∑ i ∈ Icc 1 n, log (i : ℝ)) ≤ F n + 1 + log n := by induction n, hn using Nat.le_induction with | base => norm_num [F] | succ n hn ih => have hn0 : (0 : ℝ) < n := by exact_mod_cast (show 0 < n by omega) obtain ⟨hlo, hhi⟩ := difference_bounds hn0 (show 0 < (n : ℝ) + 1 by positivity) have heq : (n : ℝ) + 1 - n = 1 := by ring rw [heq, one_mul] at hlo hhi rw [Finset.sum_Icc_succ_top (by omega)] push_cast constructor <;> linarith /-- Bounds for the logarithmic sum at a real endpoint, using only finite sums and the elementary tangent inequalities for the logarithm. -/ theorem real_sum_bounds {x : ℝ} (hx : 1 ≤ x) : x * log x - x + 1 - log x ≤ ∑ i ∈ Icc 1 ⌊x⌋₊, log (i : ℝ) ∧ (∑ i ∈ Icc 1 ⌊x⌋₊, log (i : ℝ)) ≤ x * log x - x + 1 + log x := by have hn : 1 ≤ ⌊x⌋₊ := Nat.le_floor (by simpa using hx) have hn0 : (0 : ℝ) < ⌊x⌋₊ := by exact_mod_cast (show 0 < ⌊x⌋₊ by omega) have hx0 : 0 < x := by linarith have hnle : (⌊x⌋₊ : ℝ) ≤ x := Nat.floor_le hx0.le have hxlt : x < (⌊x⌋₊ : ℝ) + 1 := Nat.lt_floor_add_one x have hln : 0 ≤ log (⌊x⌋₊ : ℝ) := Real.log_nonneg (by exact_mod_cast hn) have hlx : 0 ≤ log x := Real.log_nonneg hx have hlogle : log (⌊x⌋₊ : ℝ) ≤ log x := Real.log_le_log hn0 hnle obtain ⟨hlo, hhi⟩ := difference_bounds hn0 hx0 have hnonneg := mul_nonneg (sub_nonneg.mpr hnle) hln have hFmono : F (⌊x⌋₊ : ℝ) ≤ F x := by linarith have hprod := mul_le_mul_of_nonneg_right (show x - (⌊x⌋₊ : ℝ) ≤ 1 by linarith) hlx have hFnear : F x - F (⌊x⌋₊ : ℝ) ≤ log x := by linarith obtain ⟨hslo, hshi⟩ := nat_sum_bounds ⌊x⌋₊ hn dsimp [F] at hFmono hFnear hslo hshi constructor <;> linarith end Bounty.LogSum end end /- Proof component: ElementaryCompatibility -/ section /- Ported and simplified from AlexKontorovich/PrimeNumberTheoremAnd, IEANTN/Chebyshev.lean, commit c39a751132c88b6e8080b74c74023fd95b3d8be0. The upstream numerical tables and native-decide certificate are not used. -/ namespace Bounty.ElementaryChebyshev open Chebyshev open Real Finsupp Finset open ArithmeticFunction hiding log private lemma Ioc_nat_eq_Icc (M N : ℕ) : Finset.Ioc N M = Finset.Icc (N + 1) M := by ext n simp only [Finset.mem_Ioc, Finset.mem_Icc] omega noncomputable def T (x : ℝ) : ℝ := ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, log n theorem T.le (x : ℝ) (hx : 1 ≤ x) : T x ≤ x * log x - x + 1 + log x := by exact (Bounty.LogSum.real_sum_bounds hx).2 theorem T.ge (x : ℝ) (hx : 1 ≤ x) : T x ≥ x * log x - x + 1 - log x := by exact (Bounty.LogSum.real_sum_bounds hx).1 theorem T.eq_sum_Lambda (x : ℝ) : T x = ∑ n ∈ Icc 1 ⌊x⌋₊, ArithmeticFunction.vonMangoldt n * ⌊x / n⌋₊ := by unfold T simp_rw [← log_apply, ← vonMangoldt_mul_zeta] rw [← Ioc_nat_eq_Icc, sum_Ioc_mul_zeta_eq_sum] simp [Nat.floor_div_natCast] noncomputable def E (ν : ℕ →₀ ℝ) (x : ℝ) : ℝ := ν.sum (fun m w ↦ w * ⌊ x / m ⌋₊) theorem T.weighted_eq_sum (ν : ℕ →₀ ℝ) (x : ℝ) : ν.sum (fun m w ↦ w * T (x/m)) = ∑ n ∈ Icc 1 ⌊x⌋₊, ArithmeticFunction.vonMangoldt n * E ν (x/n) := by simp_rw [T.eq_sum_Lambda, E, Finsupp.mul_sum] rw [← sum_finsetSum_comm] apply Finsupp.sum_congr fun y hy ↦ ?_ rw [Finset.mul_sum] by_cases hy : y = 0 · simp [hy] have one_le_y : 1 ≤ (y : ℝ) := by grind [Nat.one_le_cast] by_cases hx : x < 1 · simp [hx, show x / y < 1 from div_lt_one (by linarith)|>.mpr (by linarith)] apply sum_subset_zero_on_sdiff · apply Icc_subset_Icc_right gcongr exact div_le_self (by linarith) one_le_y · intro t ht simp only [mem_sdiff, mem_Icc, not_and, not_le] at ht simp only [mul_eq_zero, Nat.cast_eq_zero, Nat.floor_eq_zero] right right apply div_lt_one (by linarith)|>.mpr have := ht.2 ht.1.1 apply div_lt_iff₀ (by simp; grind)|>.mpr rw [Nat.floor_lt <| div_nonneg (by linarith) (by linarith)] at this have := div_lt_iff₀ (by linarith)|>.mp this rwa [mul_comm] at this · grind open Finsupp in noncomputable def ν : ℕ →₀ ℝ := single 1 1 - single 2 1 - single 3 1 - single 5 1 + single 30 1 /-- The support of `ν` is `{1, 2, 3, 5, 30}`. Used whenever we need to unfold `ν.sum`. -/ private lemma ν_support : ν.support = {1, 2, 3, 5, 30} := by norm_num [ν, Finset.ext_iff]; grind /-- Unfold `ν.sum (fun m w ↦ w * f m)` into its five-term expansion. This avoids repeating the `sum_add_index` / `sum_sub_index` chain every time we need to compute a `ν`-weighted sum. -/ private lemma ν_sum_mul (f : ℕ → ℝ) : ν.sum (fun m w ↦ w * f m) = f 1 - f 2 - f 3 - f 5 + f 30 := by rw [ν, sum_add_index (by simp) (by intros; ring)] grind only [sum_single_index, sum_sub_index] /-- Unfold `E ν y` into an explicit expression in terms of floors of `y / k`. This is the key formula repeatedly used to analyse `E ν`. -/ private lemma E_nu_expand (y : ℝ) : E ν y = ⌊y⌋₊ - ⌊y / 2⌋₊ - ⌊y / 3⌋₊ - ⌊y / 5⌋₊ + ⌊y / 30⌋₊ := by rw [E, ν, sum_add_index' (by grind) (by grind)] grind [sum_single_index, sum_sub_index] /-- The classical sandwich `k * ⌊y/k⌋₊ ≤ ⌊y⌋₊ < k * ⌊y/k⌋₊ + k` for `k ≥ 1` and `y ≥ 0`. -/ private lemma floor_div_bounds {y : ℝ} (hy : 0 ≤ y) {k : ℕ} (hk : 1 ≤ k) : k * ⌊y / k⌋₊ ≤ ⌊y⌋₊ ∧ ⌊y⌋₊ < k * ⌊y / k⌋₊ + k := by have hk' : (0 : ℝ) < k := by exact_mod_cast hk have hdivnn : 0 ≤ y / k := div_nonneg hy hk'.le refine ⟨Nat.le_floor ?_, ?_⟩ · push_cast have := Nat.floor_le hdivnn calc ((k : ℝ) * ⌊y / k⌋₊) = k * (y / k) - k * (y / k - ⌊y / k⌋₊) := by ring _ ≤ k * (y / k) := by nlinarith [Nat.floor_le hdivnn] _ = y := mul_div_cancel₀ _ hk'.ne' · have hlt : y / k < ⌊y / k⌋₊ + 1 := Nat.lt_floor_add_one (y / k) have hy_lt : y < (k : ℝ) * (⌊y / k⌋₊ + 1) := by linarith [(div_lt_iff₀ hk').mp hlt] have : (⌊y⌋₊ : ℝ) < (k : ℝ) * (⌊y / k⌋₊ + 1) := (Nat.floor_le hy).trans_lt hy_lt exact_mod_cast this theorem nu_sum_div_eq_zero : ν.sum (fun n w ↦ w / n) = 0 := by norm_num [ν, add_div, sum_add_index', sub_div, sum_sub_index] theorem E_nu_eq_one (x : ℝ) (hx : x ∈ Set.Ico 1 6) : E ν x = 1 := by obtain ⟨h1, h6⟩ := hx have hx0 : (0 : ℝ) ≤ x := by linarith simp only [E_nu_expand, Nat.floor_eq_zero.mpr (by linarith : x / 30 < 1)] have hflb : 1 ≤ ⌊x⌋₊ := by rwa [Nat.one_le_floor_iff] have hfub : ⌊x⌋₊ ≤ 5 := Nat.lt_succ_iff.mp (Nat.floor_lt' (by grind) |>.mpr h6) have h2 := floor_div_bounds hx0 (k := 2) (by norm_num) have h3 := floor_div_bounds hx0 (k := 3) (by norm_num) have h5 := floor_div_bounds hx0 (k := 5) (by norm_num) push_cast at h2 h3 h5 rw [show ⌊x⌋₊ = ⌊x / 2⌋₊ + ⌊x / 3⌋₊ + ⌊x / 5⌋₊ + 1 by omega] grind theorem E_nu_period (x : ℝ) (hx : x ≥ 0) : E ν (x + 30) = E ν x := by have h (k : ℝ) : (x + 30) / k = x / k + (30 / k) := by ring simp_rw [E_nu_expand, h 2, h 3, h 5, h 30] norm_num repeat rw [Nat.floor_add_ofNat (by positivity)] rw [Nat.floor_add_one (by positivity)] grind theorem E_nu_bound (x : ℝ) (hx : x ≥ 0) : 0 ≤ E ν x ∧ E ν x ≤ 1 := by have : ∀ y, 0 ≤ y → y < 30 → 0 ≤ E ν y ∧ E ν y ≤ 1 := fun y hy0 hy30 ↦ by simp only [E_nu_expand, Nat.floor_eq_zero.mpr (by linarith : y / 30 < 1), Nat.cast_zero, add_zero] have h2 := floor_div_bounds hy0 (k := 2) (by norm_num) have h3 := floor_div_bounds hy0 (k := 3) (by norm_num) have h5 := floor_div_bounds hy0 (k := 5) (by norm_num) push_cast at h2 h3 h5 have hfy : ⌊y⌋₊ < 30 := Nat.floor_lt' (by norm_num) |>.mpr (by exact_mod_cast hy30) have hlb : ⌊y/2⌋₊ + ⌊y/3⌋₊ + ⌊y/5⌋₊ ≤ ⌊y⌋₊ := by omega have hub : ⌊y⌋₊ ≤ ⌊y/2⌋₊ + ⌊y/3⌋₊ + ⌊y/5⌋₊ + 1 := by omega have hlb' : ((⌊y/2⌋₊ + ⌊y/3⌋₊ + ⌊y/5⌋₊ : ℕ) : ℝ) ≤ (⌊y⌋₊ : ℝ) := by exact_mod_cast hlb have hub' : ((⌊y⌋₊ : ℕ) : ℝ) ≤ ((⌊y/2⌋₊ + ⌊y/3⌋₊ + ⌊y/5⌋₊ + 1 : ℕ) : ℝ) := by exact_mod_cast hub push_cast at hlb' hub' refine ⟨by linarith, by linarith⟩ let y := x - ⌊x / 30⌋₊ * 30 have hy : 0 ≤ y ∧ y < 30 := ⟨by linarith [Nat.floor_le (by positivity : 0 ≤ x/30)], by linarith [Nat.lt_floor_add_one (x/30)]⟩ have hxy : E ν x = E ν y := by have : x = y + ⌊x/30⌋₊ * 30 := by ring rw [this]; induction ⌊x/30⌋₊ with | zero => simp | succ n ih => simp [add_mul, ← add_assoc, E_nu_period _ (by linarith : y + n * 30 ≥ 0), ih] exact hxy ▸ this y hy.1 hy.2 noncomputable def U (x : ℝ) : ℝ := ν.sum (fun m w ↦ w * T (x/m)) theorem psi_ge_weighted (x : ℝ) (hx : x > 0) : Chebyshev.psi x ≥ U x := by unfold U psi rw [T.weighted_eq_sum, ← Ioc_nat_eq_Icc] gcongr with i have := E_nu_bound (x / i) (div_nonneg hx.le (by simp)) grw [this.2, mul_one] exact ArithmeticFunction.vonMangoldt_nonneg theorem psi_diff_le_weighted (x : ℝ) (hx : x > 0) : Chebyshev.psi x - Chebyshev.psi (x / 6) ≤ U x := by unfold U psi rw [T.weighted_eq_sum, ← Ioc_nat_eq_Icc] have subset : Ioc 0 ⌊x / 6⌋₊ ⊆ Ioc 0 ⌊x⌋₊ := by apply Ioc_subset_Ioc_right gcongr exact div_le_self hx.le (by norm_num) rw [← sum_sdiff_eq_sub subset, ← sum_sdiff subset] refine le_add_of_le_of_nonneg (sum_le_sum fun n hn ↦ ?_) (sum_nonneg fun n hn ↦ mul_nonneg vonMangoldt_nonneg ?_) · rw [E_nu_eq_one, mul_one] simp_all only [gt_iff_lt, Finset.mem_sdiff, Finset.mem_Ioc, not_and, not_le, Set.mem_Ico] refine ⟨one_le_div (by simp; grind)|>.mpr <| Nat.le_floor_iff hx.le |>.mp hn.1.2, ?_⟩ have := hn.2 hn.1.1 apply div_lt_iff₀ (by simp; grind)|>.mpr rw [Nat.floor_lt <| div_nonneg (by linarith) (by linarith)] at this have := div_lt_iff₀ (by linarith)|>.mp this rwa [mul_comm] at this · exact E_nu_bound _ (div_nonneg hx.le (by simp))|>.1 noncomputable def a : ℝ := - ν.sum (fun m w ↦ w * log m / m) lemma a_simpl : a = (7/15) * Real.log 2 + (3/10) * Real.log 3 + (1/6) * Real.log 5 := by norm_num [a, Finsupp.sum, single_apply, ν_support] norm_num [Finset.sum, ν] grind [show (30 : ℝ) = 2 * 3 * 5 by ring, log_mul, log_mul] theorem a_lower : (17 / 30 : ℝ) ≤ a := by rw [a_simpl] have h2 := Real.one_sub_inv_le_log_of_pos (by norm_num : (0 : ℝ) < 2) have h3 := Real.one_sub_inv_le_log_of_pos (by norm_num : (0 : ℝ) < 3) have h5 := Real.one_sub_inv_le_log_of_pos (by norm_num : (0 : ℝ) < 5) norm_num at h2 h3 h5 linarith noncomputable def e (x : ℝ) : ℝ := (T x - (x * log x - x + 1)) lemma U_bound.lemma_1 (x : ℝ) : T x = x * log x - x + 1 + (e x) := by unfold e ring lemma U_bound.lemma_2 (x : ℝ) (hx : 1 ≤ x) : |e x| ≤ log x := by rw [abs_le] unfold e constructor <;> linarith [T.ge x hx, T.le x hx] lemma U_bound.lemma_3 (x : ℝ) : U x = ν.sum (fun m w ↦ w * ((x / m) * (log (x / m)))) - ν.sum (fun m w ↦ w * (x / m)) + ν.sum (fun _m w ↦ w) + ν.sum (fun m w ↦ w * e (x / m)) := by simp [U, Finsupp.sum, U_bound.lemma_1, sub_eq_add_neg, add_mul, mul_comm, sum_add_distrib] lemma U_bound.lemma_4 (x : ℝ) (hx : 0 < x) : ν.sum (fun m w ↦ w * ((x / m) * log (x / m))) = a * x := by have hx0 : x ≠ 0 := ne_of_gt hx have ha : a = -(log 1 / 1 - log 2 / 2 - log 3 / 3 - log 5 / 5 + log 30 / 30) := by simp_rw [a, mul_div_assoc]; rw [ν_sum_mul (fun m ↦ log m / m)]; push_cast; rfl rw [ν_sum_mul (fun m ↦ (x / m) * log (x / m)), ha] simp [Real.log_div hx0] ring lemma U_bound.lemma_5 (x : ℝ) : ν.sum (fun m w ↦ w * (x / m)) = 0 := by rw [ν_sum_mul (fun m ↦ x / m)]; push_cast; ring lemma U_bound.lemma_6 : ν.sum (fun _ w ↦ w) = (-1 : ℝ) := by have := ν_sum_mul (fun _ ↦ (1 : ℝ)); simp at this; linarith lemma Finsupp.abs_sum_le (A : Type*) (ν : A →₀ ℝ) (g : A → ℝ → ℝ) : |ν.sum g| ≤ ν.sum |g| := by simp_rw [Finsupp.sum.eq_1] exact abs_sum_le_sum_abs (fun i ↦ g i (ν i)) ν.support theorem U_bound (x : ℝ) (hx : 30 ≤ x) : |U x - a * x| ≤ 5 * log x + 1 := by have hxpos : 0 < x := lt_of_lt_of_le (by norm_num) hx rw [U_bound.lemma_3, U_bound.lemma_4 x hxpos] ring_nf have hlin : ν.sum (fun m w ↦ x * w * (↑m)⁻¹) = 0 := by simpa [div_eq_mul_inv, mul_assoc, mul_left_comm] using U_bound.lemma_5 x rw [hlin]; ring_nf; rw [U_bound.lemma_6] grw [abs_add_le, Finsupp.abs_sum_le] norm_num have hsupp_eq : ν.support = {1, 2, 3, 5, 30} := ν_support have hmem_of_supp : ∀ i ∈ ν.support, 0 < i ∧ i ≤ 30 := fun i hi ↦ by have : i ∈ ({1, 2, 3, 5, 30} : Finset ℕ) := hsupp_eq ▸ hi simp only [mem_insert, mem_singleton] at this constructor <;> omega have h : ν.sum |fun m w ↦ w * e (x * (↑m)⁻¹)| ≤ ν.sum (fun m w ↦ |w| * log (x * (↑m)⁻¹)) := by apply Finsupp.sum_le_sum intro i hi simp only [Pi.abs_apply, abs_mul] obtain ⟨hi_pos, hi_le⟩ := hmem_of_supp i hi have hxi : 1 ≤ x * (↑i)⁻¹ := by rw [le_mul_inv_iff₀ (by exact_mod_cast hi_pos)] linarith [show (i : ℝ) ≤ 30 from by exact_mod_cast hi_le] gcongr; exact U_bound.lemma_2 _ hxi grw [h] have hlog_split : ν.sum (fun m w ↦ |w| * log (x * (m : ℝ)⁻¹)) = log x * ν.sum (fun m w ↦ |w|) - ν.sum (fun m w ↦ |w| * log (↑m : ℝ)) := by simp only [Finsupp.sum] conv_rhs => rw [Finset.mul_sum, ← sum_sub_distrib] apply Finset.sum_congr rfl intro m hm have hm_pos : (0 : ℝ) < m := by exact_mod_cast (hmem_of_supp m hm).1 rw [← div_eq_mul_inv, Real.log_div (ne_of_gt hxpos) (ne_of_gt hm_pos)]; ring rw [hlog_split] -- Once the support of `ν` is known explicitly, both `habs` and `hsum_eq` -- reduce to concrete arithmetic over a five-element finset. have expand_sum : ∀ f : ℕ → ℝ → ℝ, (∀ n, f n 0 = 0) → ν.sum f = f 1 1 + f 2 (-1) + f 3 (-1) + f 5 (-1) + f 30 1 := by intro f hf rw [Finsupp.sum_of_support_subset _ hsupp_eq.le _ (by intros; simp [hf])] simp only [sum_insert (by decide : (1:ℕ) ∉ ({2,3,5,30} : Finset ℕ)), sum_insert (by decide : (2:ℕ) ∉ ({3,5,30} : Finset ℕ)), sum_insert (by decide : (3:ℕ) ∉ ({5,30} : Finset ℕ)), sum_insert (by decide : (5:ℕ) ∉ ({30} : Finset ℕ)), sum_singleton, ν, Finsupp.sub_apply, Finsupp.add_apply, Finsupp.single_apply] norm_num ring have habs : ν.sum (fun m w ↦ |w|) = 5 := by rw [expand_sum _ (by intros; simp)]; norm_num have hgeq0 : 0 ≤ ν.sum (fun m w ↦ |w| * log m) := by apply Finsupp.sum_nonneg intro m hm exact mul_nonneg (abs_nonneg _) (Real.log_nonneg (by exact_mod_cast (hmem_of_supp m hm).1)) rw [habs]; linarith theorem psi_lower (x : ℝ) (hx : 30 ≤ x) : Chebyshev.psi x ≥ a * x - 5 * log x - 1 := by have h2 := abs_sub_le_iff.mp (U_bound x hx) linarith [psi_ge_weighted x (by linarith), h2.1] theorem psi_diff_upper (x : ℝ) (hx : 30 ≤ x) : Chebyshev.psi x - Chebyshev.psi (x / 6) ≤ a * x + 5 * log x + 1 := by have h2 := abs_sub_le_iff.mp (U_bound x hx) linarith [psi_diff_le_weighted x (by linarith), h2.2] lemma log_le_two_sqrt {x : ℝ} (hx : 0 ≤ x) : log x ≤ 2 * √x := by have hh := Real.log_le_rpow_div hx (by norm_num : (0 : ℝ) < 1 / 2) rw [← Real.sqrt_eq_rpow] at hh linarith /-- A coarse explicit global upper bound obtained by elementary induction. The generous square-root error avoids all numerical log tables. -/ theorem psi_upper_sqrt (x : ℝ) (hx : 0 ≤ x) : Chebyshev.psi x ≤ (6 / 5) * a * x + 100 * √x := by have ha : 0 ≤ a := by linarith [a_lower] have hlog4 : log (4 : ℝ) ≤ 2 := by have hlog2 := Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 2) have heq : log (4 : ℝ) = 2 * log 2 := by rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow] norm_num linarith have hNat : ∀ n : ℕ, Chebyshev.psi (n : ℝ) ≤ (6 / 5) * a * n + 100 * √(n : ℝ) := by intro n induction n using Nat.strong_induction_on with | h n ih => have hn0 : (0 : ℝ) ≤ n := Nat.cast_nonneg _ have hs0 : 0 ≤ √(n : ℝ) := Real.sqrt_nonneg _ have hs2 : √(n : ℝ) ^ 2 = (n : ℝ) := Real.sq_sqrt hn0 by_cases hsmall : n ≤ 30 · have hbound := Chebyshev.psi_le_const_mul_self hn0 have hn30 : (n : ℝ) ≤ 30 := by exact_mod_cast hsmall have hs6 : √(n : ℝ) ≤ 6 := (Real.sqrt_le_iff).mpr ⟨by norm_num, by linarith⟩ have hmul := mul_le_mul_of_nonneg_right hs6 hs0 have ha' : 0 ≤ (6 / 5) * a * (n : ℝ) := by positivity have hlog' := mul_le_mul_of_nonneg_right hlog4 hn0 nlinarith · have hn30 : (30 : ℝ) ≤ n := by exact_mod_cast (show 30 ≤ n by omega) let t := ⌊(n : ℝ) / 6⌋₊ have ht_le : (t : ℝ) ≤ (n : ℝ) / 6 := Nat.floor_le (by positivity) have ht_lt : t < n := by have hh : (t : ℝ) < n := ht_le.trans_lt (by linarith) exact_mod_cast hh have hhalf : Chebyshev.psi ((n : ℝ) / 6) ≤ (6 / 5) * a * ((n : ℝ) / 6) + 100 * √((n : ℝ) / 6) := by rw [Chebyshev.psi_eq_psi_coe_floor] have hi := ih t ht_lt change Chebyshev.psi (t : ℝ) ≤ _ calc Chebyshev.psi (t : ℝ) ≤ (6 / 5) * a * (t : ℝ) + 100 * √(t : ℝ) := hi _ ≤ _ := by gcongr have hroot : √((n : ℝ) / 6) ≤ √(n : ℝ) / 2 := by apply Real.sqrt_le_iff.mpr constructor · positivity · nlinarith have hone : 1 ≤ √(n : ℝ) := by calc (1 : ℝ) = √(1 : ℝ) := by norm_num _ ≤ √(n : ℝ) := Real.sqrt_le_sqrt (by linarith) have hlog := log_le_two_sqrt hn0 have hdiff := psi_diff_upper (n : ℝ) hn30 nlinarith rw [Chebyshev.psi_eq_psi_coe_floor] calc Chebyshev.psi (⌊x⌋₊ : ℝ) ≤ (6 / 5) * a * (⌊x⌋₊ : ℝ) + 100 * √(⌊x⌋₊ : ℝ) := hNat _ _ ≤ _ := by gcongr <;> exact Nat.floor_le hx /-- A deliberately coarse logarithm estimate valid from the explicit threshold used for the finite prime ladder. -/ theorem log_le_sqrt_div_200 {x : ℝ} (hx : 100000000 ≤ x) : log x ≤ √x / 200 := by have hx0 : 0 < x := by linarith have hs : 10000 ≤ √x := by have hh := Real.sqrt_le_sqrt hx norm_num at hh exact hh have hlog2 : log (2 : ℝ) ≤ 1 := by have hh := Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 2) linarith have hlog10000 : log (10000 : ℝ) ≤ 14 := by calc log (10000 : ℝ) ≤ log ((2 : ℝ) ^ (14 : ℕ)) := Real.log_le_log (by norm_num) (by norm_num) _ = 14 * log (2 : ℝ) := by rw [Real.log_pow]; norm_num _ ≤ 14 := by linarith have hratio := Real.log_le_sub_one_of_pos (div_pos (Real.sqrt_pos.mpr hx0) (by norm_num : (0 : ℝ) < 10000)) rw [Real.log_div (ne_of_gt (Real.sqrt_pos.mpr hx0)) (by norm_num), Real.log_sqrt hx0.le] at hratio linarith lemma sqrt_le_div_10000 {x : ℝ} (hx : 100000000 ≤ x) : √x ≤ x / 10000 := by have hx0 : 0 ≤ x := by linarith have hs : 10000 ≤ √x := by have hh := Real.sqrt_le_sqrt hx norm_num at hh exact hh have hmul := mul_le_mul_of_nonneg_right hs (Real.sqrt_nonneg x) nlinarith [Real.sq_sqrt hx0] /-- Explicit lower bound for the first Chebyshev function after the finite prime-ladder threshold. -/ theorem theta_lower_large {x : ℝ} (hx : 100000000 ≤ x) : a * x - (11 / 1000) * x ≤ Chebyshev.theta x := by have hlog := log_le_sqrt_div_200 hx have hroot := sqrt_le_div_10000 hx have hx0 : 0 ≤ x := by linarith have hprod := mul_le_mul_of_nonneg_left hlog (show 0 ≤ 2 * √x by positivity) have hsquare := Real.sq_sqrt hx0 have herror : 2 * √x * log x ≤ x / 100 := by nlinarith have hsmall : 5 * log x + 1 ≤ x / 1000 := by linarith have hpsi := psi_lower x (by linarith) have hdiff := Chebyshev.psi_sub_theta_le (x := x) (by linarith) linarith theorem theta_upper_large {x : ℝ} (hx : 100000000 ≤ x) : Chebyshev.theta x ≤ (6 / 5) * a * x + x / 100 := by have hpsi := psi_upper_sqrt x (by linarith) have htheta := Chebyshev.theta_le_psi x have hroot := sqrt_le_div_10000 hx linarith /-- The first Chebyshev function increases on every quarter-length interval past the explicit threshold. -/ theorem theta_quarter_increase {x : ℝ} (hx : 100000000 ≤ x) : Chebyshev.theta x < Chebyshev.theta ((5 / 4) * x) := by have hy : 100000000 ≤ (5 / 4 : ℝ) * x := by linarith have hlo := theta_lower_large hy have hhi := theta_upper_large hx have ha := mul_le_mul_of_nonneg_right a_lower (show 0 ≤ x by linarith) nlinarith /-- An increase of `theta` forces a prime in the corresponding interval. -/ theorem prime_of_theta_increase {x y : ℝ} (hy : 0 ≤ y) (hinc : Chebyshev.theta x < Chebyshev.theta y) : ∃ p : ℕ, p.Prime ∧ x < p ∧ (p : ℝ) ≤ y := by classical by_contra hno have hsub : (Finset.Icc 0 ⌊y⌋₊).filter Nat.Prime ⊆ (Finset.Icc 0 ⌊x⌋₊).filter Nat.Prime := by intro p hp simp only [Finset.mem_filter, Finset.mem_Icc] at hp ⊢ have hpy : (p : ℝ) ≤ y := (Nat.cast_le.mpr hp.1.2).trans (Nat.floor_le hy) have hpx : (p : ℝ) ≤ x := by by_contra hh exact hno ⟨p, hp.2, lt_of_not_ge hh, hpy⟩ exact ⟨⟨Nat.zero_le p, Nat.le_floor hpx⟩, hp.2⟩ have hle : Chebyshev.theta y ≤ Chebyshev.theta x := by rw [Chebyshev.theta_eq_sum_Icc, Chebyshev.theta_eq_sum_Icc] apply Finset.sum_le_sum_of_subset_of_nonneg hsub intro p hp _ have hpprime := (Finset.mem_filter.mp hp).2 exact Real.log_nonneg (by exact_mod_cast hpprime.one_le) exact (not_lt_of_ge hle) hinc /-- Fully checked prime existence in every quarter-length interval from `10^8` onward, using only the elementary weighted Chebyshev argument. -/ theorem quarter_interval_large {n : ℕ} (hn : 100000000 ≤ n) : ∃ p : ℕ, p.Prime ∧ n < p ∧ 4 * p < 5 * n := by have hnreal : (100000000 : ℝ) ≤ n := by exact_mod_cast hn obtain ⟨p, hp, hpgt, hple⟩ := prime_of_theta_increase (by positivity) (theta_quarter_increase hnreal) have hpn : n < p := by exact_mod_cast hpgt have hweak : 4 * p ≤ 5 * n := by have hh : (4 : ℝ) * p ≤ 5 * n := by linarith exact_mod_cast hh have hstrict : 4 * p < 5 * n := by by_contra hnot have heq : 4 * p = 5 * n := by omega have hdiv : 5 ∣ 4 * p := by rw [heq]; exact Nat.dvd_mul_right _ _ have h5p : 5 ∣ p := ((by norm_num : Nat.Prime 5).dvd_mul.mp hdiv).resolve_left (by decide) have hp5 : p = 5 := ((Nat.dvd_prime hp).mp h5p).resolve_left (by decide) |>.symm omega exact ⟨p, hp, hpn, hstrict⟩ end Bounty.ElementaryChebyshev end /- Proof component: PrimePairComplete -/ section namespace Bounty.PrimePair /-- Every integral starting point at least 26 has a prime strictly before five quarters of that starting point. The bounded range uses an explicit prime ladder; the remaining range uses elementary Chebyshev estimates. -/ theorem quarter_interval {y : ℕ} (hy : 26 ≤ y) : ∃ p : ℕ, p.Prime ∧ y < p ∧ 4 * p < 5 * y := by by_cases hsmall : y < 100000000 · exact Bounty.PrimeLadder.quarter_interval_below_limit hy hsmall · exact Bounty.ElementaryChebyshev.quarter_interval_large (by omega) /-- The final doubling/tripling mixed configuration is impossible for every deficit. All prime-interval and smooth-base requirements are discharged. -/ theorem final_mixed_case_impossible {b h r s : ℕ} (hb : 2 ≤ b) (hbh : 3 * b ≤ h) (hgcd : Nat.gcd r s = 2) (hhs : Nat.Coprime h s) (h3 : 3 ∣ s) (hwindow : ∀ y : ℕ, b ≤ y → y < 3 * b → ¬ Nat.Coprime y s) (hunique : ∀ z : ℕ, 2 * h + b ≤ z → z < 2 * (2 * h + b) → Nat.Coprime z r → z = 3 * h) : False := by exact unique_unit_impossible_of_quarter_intervals (fun _ => quarter_interval) hb hbh hgcd hhs h3 hwindow hunique end Bounty.PrimePair end namespace Bounty.Arithmetic theorem elementary_separation_bound {v s k : ℕ} (hv : 60000 ≤ v) (hs : 0 < s) (hsv : s < 2*v) (hdiv : primorial k ∣ s) : 8*k*((v.primeFactors.card+1)*2^v.primeFactors.card) Bounty.PrimePair.quarter_interval) hv hs hsv hdiv end Bounty.Arithmetic /- Proof component: LargeWindow -/ section noncomputable section namespace Bounty.LargeWindow open Math15.LonelyRunner Arithmetic CoprimeGaps theorem large_window_valid {n r s m k:ℕ} (hn : 120000≤n) (hr : 0