subdivision_is_binary

formal source

  84
  85def subdivisionLevels : List ℕ := [1, 2, 4, 8]
  86
  87theorem subdivision_is_binary :
  88    subdivisionLevels = [2^0, 2^1, 2^2, 2^3] := by
  89  simp [subdivisionLevels]
  90
  91/-! ## Swing as Asymmetry
  92
  93"Swing" in jazz/blues displaces the second note of each pair.
  94A 2:1 swing ratio means the first eighth note lasts twice as long
  95as the second — introducing a φ-like asymmetry into the rhythm. -/
  96
  97noncomputable def swingRatio_triplet : ℝ := 2
  98noncomputable def swingRatio_moderate : ℝ := 3 / 2
  99
 100theorem swing_triplet_is_octave_ratio :
 101    swingRatio_triplet = 2 := rfl
 102
 103theorem swing_moderate_is_fifth :
 104    swingRatio_moderate = 3 / 2 := rfl
 105
 106end IndisputableMonolith.MusicTheory.Rhythm