`ticksPerCycle`

definition

show as: view math explainer →

module: IndisputableMonolith.MusicTheory.Rhythm
domain: MusicTheory
line: 20 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.MusicTheory.Rhythm on GitHub at line 20.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.