IndisputableMonolith.MusicTheory.Rhythm

   1/-
   2  MusicTheory/Rhythm.lean
   3
   4  RHYTHM FROM THE 8-TICK CYCLE
   5
   6  Common time (4/4) has 8 eighth notes per measure — this IS the 8-tick
   7  cycle of RS. Musical tempo maps rhythmic subdivisions into the 5-35 Hz
   8  DFT-8 mode frequency range, creating the physical mechanism by which
   9  rhythm entrains neural oscillations.
  10
  11  Part of: IndisputableMonolith/MusicTheory/
  12-/
  13
  14import Mathlib
  15
  16namespace IndisputableMonolith.MusicTheory.Rhythm
  17
  18/-! ## 8-Tick Beat Structure -/
  19
  20@[simp] def ticksPerCycle : ℕ := 8
  21
  22theorem eight_ticks_from_dimension : ticksPerCycle = 2 ^ 3 := by
  23  simp [ticksPerCycle]
  24
  25theorem eighth_notes_per_measure : ticksPerCycle = 8 := rfl
  26
  27/-! ## Tempo and Frequency Mapping
  28
  29A musical tempo (BPM) combined with a rhythmic subdivision determines
  30a repetition frequency in Hz. This frequency can fall in the 5-35 Hz
  31range of DFT-8 modes, creating resonant entrainment. -/
  32
  33structure Tempo where
  34  bpm : ℝ
  35  bpm_pos : 0 < bpm
  36
  37noncomputable def Tempo.beatsPerSecond (t : Tempo) : ℝ := t.bpm / 60
  38
  39noncomputable def Tempo.tickHz (t : Tempo) : ℝ := t.beatsPerSecond * ticksPerCycle
  40
  41noncomputable def Tempo.subdivisionFreq (t : Tempo) (subdivision : ℕ) : ℝ :=
  42  t.beatsPerSecond * subdivision
  43
  44theorem Tempo.tickHz_pos (t : Tempo) : 0 < t.tickHz := by
  45  unfold tickHz beatsPerSecond
  46  have : (0 : ℝ) < 60 := by norm_num
  47  have : (0 : ℝ) < (ticksPerCycle : ℕ) := by simp
  48  exact mul_pos (div_pos t.bpm_pos (by norm_num)) (by simp)
  49
  50theorem Tempo.tickHz_eq (t : Tempo) : t.tickHz = t.bpm / 60 * 8 := by
  51  unfold tickHz beatsPerSecond ticksPerCycle
  52  ring
  53
  54/-! ## Common Tempos Produce Mode Frequencies
  55
  56Musical performance tempos typically range from 60-180 BPM.
  57Rhythmic subdivisions at these tempos produce frequencies that
  58land directly on DFT-8 mode frequencies. -/
  59
  60noncomputable def tempo_120 : Tempo := ⟨120, by norm_num⟩
  61noncomputable def tempo_150 : Tempo := ⟨150, by norm_num⟩
  62noncomputable def tempo_75 : Tempo := ⟨75, by norm_num⟩
  63
  64theorem tempo_120_beat_is_2Hz :
  65    tempo_120.beatsPerSecond = 2 := by
  66  simp [Tempo.beatsPerSecond, tempo_120]; ring
  67
  68theorem tempo_120_eighth_note_is_16Hz :
  69    tempo_120.tickHz = 16 := by
  70  simp [Tempo.tickHz, Tempo.beatsPerSecond, tempo_120]; ring
  71
  72theorem tempo_150_quarter_triplet_is_mode4 :
  73    tempo_150.subdivisionFreq 8 = 20 := by
  74  simp [Tempo.subdivisionFreq, Tempo.beatsPerSecond, tempo_150]; ring
  75
  76theorem tempo_75_sixteenth_note_is_mode1 :
  77    tempo_75.subdivisionFreq 2 = 2.5 := by
  78  simp [Tempo.subdivisionFreq, Tempo.beatsPerSecond, tempo_75]; ring
  79
  80/-! ## Rhythmic Subdivision Hierarchy
  81
  82Binary subdivision (halving) maps directly to the factor-of-2 structure
  83in the 8-tick cycle. -/
  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
 107