sync_counts

formal source

  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
  80  exact ⟨lcm_8_45_eq_360, lcm_8_45_div_8, lcm_8_45_div_45⟩
  81
  82/-- The beat-level clock-lag fraction implied by the 45-gap arithmetic: δ_time = 45/960 = 3/64. -/
  83theorem delta_time_eq_3_div_64 : (45 : ℚ) / 960 = (3 : ℚ) / 64 := by
  84  norm_num
  85
  86/-! ## Beat-level API (arithmetic mapping to 8-beat cycles). -/
  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. -/