coprimality_odd

formal source

  62
  63/-- For odd `D = 2k+1`, `D²(D+2)` is odd (a product of odd numbers),
  64    hence coprime with any power of `2`. -/
  65theorem coprimality_odd (k : ℕ) :
  66    Nat.Coprime (2 ^ (2 * k + 1)) ((2 * k + 1) ^ 2 * (2 * k + 3)) := by
  67  suffices h : Nat.Coprime 2 ((2 * k + 1) ^ 2 * (2 * k + 3)) from h.pow_left _
  68  show Nat.gcd 2 ((2 * k + 1) ^ 2 * (2 * k + 3)) = 1
  69  have hodd : (2 * k + 1) ^ 2 * (2 * k + 3) =
  70      2 * (4 * k ^ 3 + 10 * k ^ 2 + 7 * k + 1) + 1 := by ring
  71  rw [hodd]
  72  set n := 4 * k ^ 3 + 10 * k ^ 2 + 7 * k + 1
  73  rw [Nat.gcd_rec]
  74  have : (2 * n + 1) % 2 = 1 := by omega
  75  rw [this]
  76  decide
  77
  78/-- For even `D = 2k` (with `k ≥ 1`), `D²(D+2)` is even, so the gcd is `> 1`. -/
  79theorem coprimality_even_fails (k : ℕ) (hk : 0 < k) :
  80    ¬ Nat.Coprime (2 ^ (2 * k)) ((2 * k) ^ 2 * (2 * k + 2)) := by
  81  intro h
  82  have h1 : 2 ∣ 2 ^ (2 * k) := dvd_pow (dvd_refl 2) (by omega)
  83  have h2 : 2 ∣ (2 * k) ^ 2 * (2 * k + 2) := ⟨2 * k ^ 2 * (2 * k + 2), by ring⟩
  84  have h3 := Nat.dvd_gcd h1 h2
  85  rw [h] at h3
  86  exact absurd h3 (by norm_num)
  87
  88/-- At `D = 3`: `gcd(8, 45) = 1`. -/
  89theorem coprime_at_D3 : Nat.Coprime (2 ^ D) (integrationGap D) := by native_decide
  90
  91/-! ## Integration gap minus one -/
  92
  93/-- The integer `D²(D+2) - 1`. At `D = 3` this equals `44`. -/
  94def gapMinusOne (d : ℕ) : ℕ := integrationGap d - 1
  95