beats

formal source

  87namespace Beat
  88
  89/-- Minimal joint duration (in beats) for 8-beat and 45-fold patterns. -/
  90@[simp] def beats : Nat := Nat.lcm 8 45
  91
  92@[simp] lemma beats_eq_360 : beats = 360 := by
  93  simp [beats, lcm_8_45_eq_360]
  94
  95/-- Number of 8-beat cycles inside the minimal joint duration. -/
  96@[simp] lemma cycles_of_8 : beats / 8 = 45 := by
  97  simp [beats, lcm_8_45_div_8]
  98
  99/-- Number of 45-fold cycles inside the minimal joint duration. -/
 100@[simp] lemma cycles_of_45 : beats / 45 = 8 := by
 101  simp [beats, lcm_8_45_div_45]
 102
 103/-- Minimality: any time `t` that is simultaneously a multiple of 8 and 45 must be a
 104multiple of the minimal joint duration `beats` (i.e., 360). -/
 105lemma minimal_sync_divides {t : Nat} (h8 : 8 ∣ t) (h45 : 45 ∣ t) : beats ∣ t := by
 106  simpa [beats] using Nat.lcm_dvd h8 h45
 107
 108/-- Convenience form of minimality with 360 on the left. -/
 109lemma minimal_sync_360_divides {t : Nat} (h8 : 8 ∣ t) (h45 : 45 ∣ t) : 360 ∣ t := by
 110  simpa [beats_eq_360] using minimal_sync_divides (t:=t) h8 h45
 111
 112/-- No positive `n < 360` can be simultaneously divisible by 8 and 45. -/
 113lemma no_smaller_multiple_8_45 {n : Nat} (hnpos : 0 < n) (hnlt : n < 360) :
 114  ¬ (8 ∣ n ∧ 45 ∣ n) := by
 115  intro h
 116  rcases h with ⟨h8, h45⟩
 117  have h360 : 360 ∣ n := minimal_sync_360_divides (t:=n) h8 h45
 118  rcases h360 with ⟨k, hk⟩
 119  rcases Nat.eq_zero_or_pos k with rfl | hkpos
 120  · simp only [mul_zero] at hk