IndisputableMonolith.NumberTheory.Primes.Modular

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.Primes.Basic
   3import IndisputableMonolith.NumberTheory.Primes.RSConstants
   4
   5/-!
   6# Modular arithmetic and wheel filters (prime-friendly)
   7
   8This file is the starting point for modular/character tooling motivated by the theory docs
   9(e.g. mod-8 gating and wheel factorization like “wheel-840”).
  10
  11In this first slice we only formalize **soundness** of a wheel: if a number is coprime to `840`,
  12then it is not divisible by the small primes `2,3,5,7` that make up the wheel.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace NumberTheory
  17namespace Primes
  18
  19open Nat
  20
  21/-- The wheel modulus `840 = 2^3 * 3 * 5 * 7`. -/
  22def wheel840 : ℕ := 840
  23
  24/-! ### The mod-8 character χ₈ (as used in the theory docs) -/
  25
  26/-- The mod-8 character χ₈ from the theory doc:
  27
  28- χ₈(n) = 0 for `n ≡ 0,2,4,6 (mod 8)` (i.e. even residues)
  29- χ₈(n) = +1 for `n ≡ 1,7 (mod 8)`
  30- χ₈(n) = -1 for `n ≡ 3,5 (mod 8)`
  31
  32We define it on naturals using `n % 8`. -/
  33def chi8 (n : ℕ) : ℤ :=
  34  match n % 8 with
  35  | 0 | 2 | 4 | 6 => 0
  36  | 1 | 7 => 1
  37  | 3 | 5 => -1
  38  | _ => 0
  39
  40theorem chi8_periodic (n k : ℕ) : chi8 (n + 8 * k) = chi8 n := by
  41  -- `chi8` depends only on `n % 8`.
  42  unfold chi8
  43  have : (n + 8 * k) % 8 = n % 8 := by
  44    simp [Nat.add_mod]
  45  -- rewrite by the mod-8 equality and the result is definitional
  46  simp [this]
  47
  48@[simp] theorem chi8_mod0 (k : ℕ) : chi8 (8 * k) = 0 := by
  49  unfold chi8
  50  simp
  51
  52@[simp] theorem chi8_mod1 (k : ℕ) : chi8 (8 * k + 1) = 1 := by
  53  unfold chi8
  54  simp [Nat.add_mod]
  55
  56@[simp] theorem chi8_mod2 (k : ℕ) : chi8 (8 * k + 2) = 0 := by
  57  unfold chi8
  58  simp [Nat.add_mod]
  59
  60@[simp] theorem chi8_mod3 (k : ℕ) : chi8 (8 * k + 3) = -1 := by
  61  unfold chi8
  62  simp [Nat.add_mod]
  63
  64@[simp] theorem chi8_mod4 (k : ℕ) : chi8 (8 * k + 4) = 0 := by
  65  unfold chi8
  66  simp [Nat.add_mod]
  67
  68@[simp] theorem chi8_mod5 (k : ℕ) : chi8 (8 * k + 5) = -1 := by
  69  unfold chi8
  70  simp [Nat.add_mod]
  71
  72@[simp] theorem chi8_mod6 (k : ℕ) : chi8 (8 * k + 6) = 0 := by
  73  unfold chi8
  74  simp [Nat.add_mod]
  75
  76@[simp] theorem chi8_mod7 (k : ℕ) : chi8 (8 * k + 7) = 1 := by
  77  unfold chi8
  78  simp [Nat.add_mod]
  79
  80/-- `chi8 n = 0` exactly when `n` is even. -/
  81theorem chi8_eq_zero_iff_even (n : ℕ) : chi8 n = 0 ↔ Even n := by
  82  -- Reduce to the remainder `r = n % 8`, which is bounded (`r < 8`).
  83  set r := n % 8 with hr
  84  have hr_lt : r < 8 := by
  85    have : n % 8 < 8 := Nat.mod_lt n (by decide)
  86    simpa [hr] using this
  87  have hchi : chi8 n = chi8 r := by
  88    -- Both sides reduce to the same `match r with ...` form.
  89    simp [chi8, hr.symm, Nat.mod_eq_of_lt hr_lt]
  90  have hhelp : (chi8 r = 0 ↔ r % 2 = 0) := by
  91    interval_cases r <;> decide
  92  have hmod : r % 2 = n % 2 := by
  93    -- `r = n % 8`, and `2 ∣ 8`, so `(n % 8) % 2 = n % 2`.
  94    simpa [hr.symm] using (mod_mod_of_dvd n (by decide : 2 ∣ 8))
  95  calc
  96    chi8 n = 0 ↔ chi8 r = 0 := by
  97      constructor
  98      · intro hn0
  99        simpa [hchi.symm] using hn0
 100      · intro hr0
 101        simpa [hchi] using hr0
 102    _ ↔ r % 2 = 0 := hhelp
 103    _ ↔ n % 2 = 0 := by
 104      constructor
 105      · intro hr0
 106        simpa [hmod] using hr0
 107      · intro hn0
 108        simpa [hmod.symm] using hn0
 109    _ ↔ Even n := by
 110      simpa using (Nat.even_iff (n := n)).symm
 111
 112/-- `chi8 n ≠ 0` exactly when `n` is odd. -/
 113theorem chi8_ne_zero_iff_odd (n : ℕ) : chi8 n ≠ 0 ↔ Odd n := by
 114  -- `chi8 n = 0 ↔ Even n`, so negate and rewrite `¬Even ↔ Odd`.
 115  simpa [Nat.not_even_iff_odd] using (not_congr (chi8_eq_zero_iff_even n))
 116
 117/-- If `n` is coprime to `840`, then none of `2,3,5,7` divide `n`. -/
 118theorem wheel840_accepts (n : ℕ) (h : Nat.Coprime n wheel840) :
 119    (¬ 2 ∣ n) ∧ (¬ 3 ∣ n) ∧ (¬ 5 ∣ n) ∧ (¬ 7 ∣ n) := by
 120  have h2 : Nat.Coprime 2 n := (h.coprime_dvd_right (by native_decide : 2 ∣ wheel840)).symm
 121  have h3 : Nat.Coprime 3 n := (h.coprime_dvd_right (by native_decide : 3 ∣ wheel840)).symm
 122  have h5 : Nat.Coprime 5 n := (h.coprime_dvd_right (by native_decide : 5 ∣ wheel840)).symm
 123  have h7 : Nat.Coprime 7 n := (h.coprime_dvd_right (by native_decide : 7 ∣ wheel840)).symm
 124  refine ⟨?_, ?_, ?_, ?_⟩
 125  · exact (Nat.Prime.coprime_iff_not_dvd prime_two).1 h2
 126  · exact (Nat.Prime.coprime_iff_not_dvd prime_three).1 h3
 127  · exact (Nat.Prime.coprime_iff_not_dvd prime_five).1 h5
 128  · exact (Nat.Prime.coprime_iff_not_dvd (by decide : Nat.Prime 7)).1 h7
 129
 130/-! ### Complement: rejection when not coprime -/
 131
 132/-- Any prime divisor of `wheel840` is one of `2,3,5,7`. -/
 133theorem prime_dvd_wheel840 {p : ℕ} (hp : Prime p) (h : p ∣ wheel840) :
 134    p = 2 ∨ p = 3 ∨ p = 5 ∨ p = 7 := by
 135  have hp' : Nat.Prime p := (prime_iff p).1 hp
 136  have h840 : p ∣ (840 : ℕ) := by
 137    simpa [wheel840] using h
 138  have hprod : p ∣ 2^3 * 3 * 5 * 7 := by
 139    simpa [wheel840_factorization] using h840
 140  have h1 : p ∣ (2^3 * 3 * 5) ∨ p ∣ 7 := (hp'.dvd_mul).1 hprod
 141  rcases h1 with h235 | h7
 142  · have h2 : p ∣ (2^3 * 3) ∨ p ∣ 5 := (hp'.dvd_mul).1 h235
 143    rcases h2 with h23 | h5
 144    · have h3 : p ∣ 2^3 ∨ p ∣ 3 := (hp'.dvd_mul).1 h23
 145      rcases h3 with h2pow | h3
 146      · have h2 : p ∣ 2 := hp'.dvd_of_dvd_pow (m := 2) (n := 3) h2pow
 147        exact Or.inl ((Nat.prime_dvd_prime_iff_eq hp' prime_two).1 h2)
 148      · exact Or.inr (Or.inl ((Nat.prime_dvd_prime_iff_eq hp' prime_three).1 h3))
 149    ·
 150      have h5prime : Nat.Prime 5 := (prime_iff 5).1 prime_five
 151      exact Or.inr (Or.inr (Or.inl ((Nat.prime_dvd_prime_iff_eq hp' h5prime).1 h5)))
 152  ·
 153    have h7prime : Nat.Prime 7 := by decide
 154    exact Or.inr (Or.inr (Or.inr ((Nat.prime_dvd_prime_iff_eq hp' h7prime).1 h7)))
 155
 156/-- If `n` is **not** coprime to `840`, then at least one of `2,3,5,7` divides `n`. -/
 157theorem wheel840_rejects (n : ℕ) (h : ¬ Nat.Coprime n wheel840) :
 158    2 ∣ n ∨ 3 ∣ n ∨ 5 ∣ n ∨ 7 ∣ n := by
 159  have hg_ne_one : Nat.gcd n wheel840 ≠ 1 := by
 160    intro hg
 161    apply h
 162    exact (Nat.coprime_iff_gcd_eq_one).2 hg
 163  obtain ⟨p, hpprime, hpdvg⟩ :=
 164    (Nat.ne_one_iff_exists_prime_dvd (n := Nat.gcd n wheel840)).1 hg_ne_one
 165  have hpdvn : p ∣ n := hpdvg.trans (Nat.gcd_dvd_left n wheel840)
 166  have hpdv840 : p ∣ wheel840 := hpdvg.trans (Nat.gcd_dvd_right n wheel840)
 167  have hp : Prime p := by
 168    simpa [Prime] using hpprime
 169  have hp_cases : p = 2 ∨ p = 3 ∨ p = 5 ∨ p = 7 :=
 170    prime_dvd_wheel840 (p := p) hp hpdv840
 171  rcases hp_cases with hp2 | hp_rest
 172  · left
 173    simpa [hp2] using hpdvn
 174  · rcases hp_rest with hp3 | hp_rest2
 175    · exact Or.inr (Or.inl (by simpa [hp3] using hpdvn))
 176    · rcases hp_rest2 with hp5 | hp7
 177      · exact Or.inr (Or.inr (Or.inl (by simpa [hp5] using hpdvn)))
 178      · exact Or.inr (Or.inr (Or.inr (by simpa [hp7] using hpdvn)))
 179
 180/-- A gcd-form of `wheel840_rejects` (sometimes more convenient in proofs). -/
 181theorem wheel840_rejects_of_gcd_ne_one (n : ℕ) (h : Nat.gcd n wheel840 ≠ 1) :
 182    2 ∣ n ∨ 3 ∣ n ∨ 5 ∣ n ∨ 7 ∣ n := by
 183  apply wheel840_rejects (n := n)
 184  intro hc
 185  apply h
 186  exact (Nat.coprime_iff_gcd_eq_one).1 hc
 187
 188end Primes
 189end NumberTheory
 190end IndisputableMonolith
 191