wheel840

formal source

  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