IndisputableMonolith.MusicTheory.HarmonicModes

   1/-
   2  MusicTheory/HarmonicModes.lean
   3
   4  HARMONIC MODES: MUSICAL INTERVALS FROM RECOGNITION SCIENCE
   5
   6  The fundamental musical intervals (octave, fifth, fourth, etc.) are
   7  superparticular ratios (n+1)/n whose RS interval cost is determined by J-cost.
   8  The octave 2:1 is the simplest non-trivial ratio; the fifth 3:2 is the
   9  lowest-cost superparticular interval.  We also include the tritone as an
  10  important non-superparticular comparator for later conflict analysis.
  11
  12  Part of: IndisputableMonolith/MusicTheory/
  13-/
  14
  15import Mathlib
  16import IndisputableMonolith.Cost
  17
  18namespace IndisputableMonolith.MusicTheory.HarmonicModes
  19
  20open Cost
  21
  22/-! ## Fundamental Intervals -/
  23
  24@[simp] noncomputable def octave : ℝ := 2
  25@[simp] noncomputable def fifth : ℝ := 3 / 2
  26@[simp] noncomputable def fourth : ℝ := 4 / 3
  27@[simp] noncomputable def majorThird : ℝ := 5 / 4
  28@[simp] noncomputable def minorThird : ℝ := 6 / 5
  29@[simp] noncomputable def tritone : ℝ := 45 / 32
  30
  31/-! ## Superparticular Ratios
  32
  33A superparticular ratio is (n+1)/n for positive n. These are the
  34building blocks of just intonation and have the simplest J-cost
  35among all ratios near a given size. -/
  36
  37noncomputable def superparticular (n : ℕ) : ℝ :=
  38  ((n : ℝ) + 1) / (n : ℝ)
  39
  40theorem superparticular_pos {n : ℕ} (hn : 0 < n) :
  41    0 < superparticular n := by
  42  unfold superparticular
  43  apply div_pos
  44  · positivity
  45  · exact Nat.cast_pos.mpr hn
  46
  47theorem superparticular_gt_one {n : ℕ} (hn : 0 < n) :
  48    1 < superparticular n := by
  49  unfold superparticular
  50  rw [one_lt_div (Nat.cast_pos.mpr hn)]
  51  linarith [show (0 : ℝ) ≤ (n : ℝ) from Nat.cast_nonneg n]
  52
  53/-! ## Interval Identification -/
  54
  55theorem octave_eq_superparticular :
  56    octave = superparticular 1 := by
  57  simp [superparticular]; norm_num
  58
  59theorem fifth_eq_superparticular :
  60    fifth = superparticular 2 := by
  61  simp [superparticular]; norm_num
  62
  63theorem fourth_eq_superparticular :
  64    fourth = superparticular 3 := by
  65  simp [superparticular]; norm_num
  66
  67theorem majorThird_eq_superparticular :
  68    majorThird = superparticular 4 := by
  69  simp [superparticular]; norm_num
  70
  71theorem minorThird_eq_superparticular :
  72    minorThird = superparticular 5 := by
  73  simp [superparticular]; norm_num
  74
  75/-! ## Positivity -/
  76
  77theorem octave_pos : (0 : ℝ) < octave := by norm_num
  78theorem fifth_pos : (0 : ℝ) < fifth := by norm_num
  79theorem fourth_pos : (0 : ℝ) < fourth := by norm_num
  80theorem majorThird_pos : (0 : ℝ) < majorThird := by norm_num
  81theorem minorThird_pos : (0 : ℝ) < minorThird := by norm_num
  82theorem tritone_pos : (0 : ℝ) < tritone := by norm_num
  83
  84/-! ## Harmonic Relationships -/
  85
  86theorem octave_times_inv : octave * octave⁻¹ = 1 := by
  87  simp
  88
  89theorem fifth_times_fourth_eq_octave :
  90    fifth * fourth = octave := by
  91  simp; ring
  92
  93theorem octave_is_two : octave = 2 := by simp
  94
  95/-! ## Musical Interval Structure -/
  96
  97structure MusicalInterval where
  98  ratio : ℝ
  99  ratio_pos : 0 < ratio
 100
 101noncomputable def MusicalInterval.jcost (i : MusicalInterval) : ℝ :=
 102  Jcost i.ratio
 103
 104noncomputable def unisonInterval : MusicalInterval :=
 105  ⟨1, by norm_num⟩
 106
 107noncomputable def octaveInterval : MusicalInterval :=
 108  ⟨octave, octave_pos⟩
 109
 110noncomputable def fifthInterval : MusicalInterval :=
 111  ⟨fifth, fifth_pos⟩
 112
 113noncomputable def fourthInterval : MusicalInterval :=
 114  ⟨fourth, fourth_pos⟩
 115
 116noncomputable def majorThirdInterval : MusicalInterval :=
 117  ⟨majorThird, majorThird_pos⟩
 118
 119noncomputable def minorThirdInterval : MusicalInterval :=
 120  ⟨minorThird, minorThird_pos⟩
 121
 122noncomputable def tritoneInterval : MusicalInterval :=
 123  ⟨tritone, tritone_pos⟩
 124
 125/-! ## J-Cost of Standard Intervals -/
 126
 127theorem unison_jcost : Jcost (1 : ℝ) = 0 := Jcost_unit0
 128
 129theorem octave_jcost : Jcost octave = 1 / 4 := by
 130  simp [Jcost]; ring
 131
 132theorem fifth_jcost : Jcost fifth = 1 / 12 := by
 133  simp [Jcost]; ring
 134
 135theorem fourth_jcost : Jcost fourth = 1 / 24 := by
 136  simp [Jcost]; ring
 137
 138theorem majorThird_jcost : Jcost majorThird = 1 / 40 := by
 139  simp [Jcost]; ring
 140
 141theorem minorThird_jcost : Jcost minorThird = 1 / 60 := by
 142  simp [Jcost]; ring
 143
 144theorem tritone_jcost : Jcost tritone = 169 / 2880 := by
 145  simp [Jcost, tritone]
 146  ring
 147
 148/-! ## 8-Tick Connection -/
 149
 150def modesPerOctave : ℕ := 8
 151
 152theorem modes_from_dimension : modesPerOctave = 2 ^ 3 := by
 153  simp [modesPerOctave]
 154
 155end IndisputableMonolith.MusicTheory.HarmonicModes
 156