minimal_sync_divides

formal source

 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
 121    omega
 122  · have : 360 ≤ 360 * k := Nat.mul_le_mul_left 360 hkpos
 123    have : 360 ≤ n := by simpa [hk] using this
 124    exact (not_le_of_gt hnlt) this
 125
 126end Beat
 127
 128-- (Moved to IndisputableMonolith/Gap45/TimeLag.lean)
 129
 130-- (Moved to IndisputableMonolith/Gap45/RecognitionBarrier.lean)
 131
 132-- (Moved to IndisputableMonolith/Gap45/GroupView.lean)
 133
 134-- (Moved to IndisputableMonolith/Gap45/AddGroupView.lean)
 135