five_dvd_45

formal source

  46@[simp] lemma nine_dvd_45 : 9 ∣ 45 := by exact ⟨5, by decide⟩
  47
  48/-- 5 ∣ 45. -/
  49@[simp] lemma five_dvd_45 : 5 ∣ 45 := by exact ⟨9, by decide⟩
  50
  51/-- 8 ∤ 45. -/
  52@[simp] lemma eight_not_dvd_45 : ¬ 8 ∣ 45 := by decide
  53
  54/-- No positive `n < 45` is simultaneously divisible by 9 and 5. -/
  55lemma no_smaller_multiple_9_5 (n : Nat) (hnpos : 0 < n) (hnlt : n < 45) :
  56  ¬ (9 ∣ n ∧ 5 ∣ n) := by
  57  intro h
  58  rcases h with ⟨h9, h5⟩
  59  have hmul : 9 * 5 ∣ n := coprime_9_5.mul_dvd_of_dvd_of_dvd h9 h5
  60  have h45 : 45 ∣ n := by simpa using hmul
  61  rcases h45 with ⟨k, hk⟩
  62  rcases (Nat.eq_zero_or_pos k) with rfl | hkpos
  63  · simp only [mul_zero] at hk
  64    omega
  65  · have : 45 ≤ 45 * k := Nat.mul_le_mul_left 45 hkpos
  66    have : 45 ≤ n := by simpa [hk] using this
  67    exact (not_le_of_gt hnlt) this
  68
  69/-- Summary: 45 is the first rung where 9- and 5-fold periodicities coincide, and it is not
  70    synchronized with the 8-beat (since 8 ∤ 45). -/
  71theorem rung45_first_conflict :
  72  (9 ∣ 45) ∧ (5 ∣ 45) ∧ ¬ 8 ∣ 45 ∧ ∀ n, 0 < n → n < 45 → ¬ (9 ∣ n ∧ 5 ∣ n) := by
  73  refine ⟨nine_dvd_45, five_dvd_45, eight_not_dvd_45, ?_⟩
  74  intro n hnpos hnlt; exact no_smaller_multiple_9_5 n hnpos hnlt
  75
  76/-- Synchronization requirement: the minimal time to jointly align 8-beat and 45-fold symmetries
  77    is exactly lcm(8,45) = 360 beats, corresponding to 45 cycles of 8 and 8 cycles of 45. -/
  78theorem sync_counts :
  79  Nat.lcm 8 45 = 360 ∧ Nat.lcm 8 45 / 8 = 45 ∧ Nat.lcm 8 45 / 45 = 8 := by