integrationGap_at_D3

formal source

  54
  55theorem parityCount_at_D3 : parityCount D = 9 := by native_decide
  56
  57theorem integrationGap_at_D3 : integrationGap D = 45 := by native_decide
  58
  59theorem integrationGap_factors : integrationGap D = 9 * 5 := by native_decide
  60
  61/-! ## Coprimality forces odd dimension -/
  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