IndisputableMonolith.MusicTheory.Consonance

   1/-
   2  MusicTheory/Consonance.lean
   3
   4  CONSONANCE IS J-COST
   5
   6  The consonance of a musical interval is determined entirely by its J-cost.
   7  No additional axiom is needed: J(r) = (r + 1/r)/2 - 1 directly measures
   8  how far a ratio deviates from unity, and this deviation IS dissonance.
   9
  10  Key result: the RS interval-cost hierarchy
  11    unison > minor third > major third > fourth > tritone > fifth > octave
  12  is proved from J-cost alone.
  13
  14  Part of: IndisputableMonolith/MusicTheory/
  15-/
  16
  17import Mathlib
  18import IndisputableMonolith.Cost
  19import IndisputableMonolith.MusicTheory.HarmonicModes
  20
  21namespace IndisputableMonolith.MusicTheory.Consonance
  22
  23open Cost
  24open HarmonicModes
  25
  26/-! ## Interval Cost (consonance measure)
  27
  28For any positive ratio r, its "interval cost" is simply J(r).
  29Lower cost = more consonant. -/
  30
  31noncomputable def intervalCost (r : ℝ) : ℝ := Jcost r
  32
  33theorem intervalCost_eq_jcost (r : ℝ) : intervalCost r = Jcost r := rfl
  34
  35/-! ## Consonance Predicate -/
  36
  37def IsConsonant (r : ℝ) (threshold : ℝ) : Prop := Jcost r < threshold
  38
  39/-! ## The Consonance Hierarchy
  40
  41Proved: J(1) < J(6/5) < J(5/4) < J(4/3) < J(45/32) < J(3/2) < J(2).
  42This is the RS ratio-cost hierarchy, derived purely from the J-cost
  43function.  It should be read as a model-side strain ordering, not as a full
  44replacement for all of human music theory. -/
  45
  46theorem jcost_unison : Jcost (1 : ℝ) = 0 := Jcost_unit0
  47
  48theorem jcost_minorThird : Jcost minorThird = 1 / 60 := HarmonicModes.minorThird_jcost
  49theorem jcost_majorThird : Jcost majorThird = 1 / 40 := HarmonicModes.majorThird_jcost
  50theorem jcost_fourth : Jcost fourth = 1 / 24 := HarmonicModes.fourth_jcost
  51theorem jcost_tritone : Jcost tritone = 169 / 2880 := HarmonicModes.tritone_jcost
  52theorem jcost_fifth : Jcost fifth = 1 / 12 := HarmonicModes.fifth_jcost
  53theorem jcost_octave : Jcost octave = 1 / 4 := HarmonicModes.octave_jcost
  54
  55theorem hierarchy_unison_lt_minorThird :
  56    Jcost (1 : ℝ) < Jcost minorThird := by
  57  rw [jcost_unison, jcost_minorThird]; norm_num
  58
  59theorem hierarchy_minorThird_lt_majorThird :
  60    Jcost minorThird < Jcost majorThird := by
  61  rw [jcost_minorThird, jcost_majorThird]; norm_num
  62
  63theorem hierarchy_majorThird_lt_fourth :
  64    Jcost majorThird < Jcost fourth := by
  65  rw [jcost_majorThird, jcost_fourth]; norm_num
  66
  67theorem hierarchy_fourth_lt_fifth :
  68    Jcost fourth < Jcost fifth := by
  69  rw [jcost_fourth, jcost_fifth]; norm_num
  70
  71theorem hierarchy_fourth_lt_tritone :
  72    Jcost fourth < Jcost tritone := by
  73  rw [jcost_fourth, jcost_tritone]; norm_num
  74
  75theorem hierarchy_tritone_lt_fifth :
  76    Jcost tritone < Jcost fifth := by
  77  rw [jcost_tritone, jcost_fifth]; norm_num
  78
  79theorem hierarchy_fifth_lt_octave :
  80    Jcost fifth < Jcost octave := by
  81  rw [jcost_fifth, jcost_octave]; norm_num
  82
  83theorem consonance_hierarchy :
  84    Jcost (1 : ℝ) < Jcost minorThird ∧
  85    Jcost minorThird < Jcost majorThird ∧
  86    Jcost majorThird < Jcost fourth ∧
  87    Jcost fourth < Jcost fifth ∧
  88    Jcost fifth < Jcost octave :=
  89  ⟨hierarchy_unison_lt_minorThird,
  90   hierarchy_minorThird_lt_majorThird,
  91   hierarchy_majorThird_lt_fourth,
  92   hierarchy_fourth_lt_fifth,
  93   hierarchy_fifth_lt_octave⟩
  94
  95theorem extended_ratio_cost_hierarchy :
  96    Jcost (1 : ℝ) < Jcost minorThird ∧
  97    Jcost minorThird < Jcost majorThird ∧
  98    Jcost majorThird < Jcost fourth ∧
  99    Jcost fourth < Jcost tritone ∧
 100    Jcost tritone < Jcost fifth ∧
 101    Jcost fifth < Jcost octave :=
 102  ⟨hierarchy_unison_lt_minorThird,
 103   hierarchy_minorThird_lt_majorThird,
 104   hierarchy_majorThird_lt_fourth,
 105   hierarchy_fourth_lt_tritone,
 106   hierarchy_tritone_lt_fifth,
 107   hierarchy_fifth_lt_octave⟩
 108
 109/-! ## Superparticular Consonance
 110
 111The J-cost of the n-th superparticular ratio (n+1)/n equals 1/(2n(n+1)).
 112This decreases with n, meaning smaller intervals are more consonant. -/
 113
 114theorem superparticular_jcost (n : ℕ) (hn : 0 < n) :
 115    Jcost (superparticular n) = 1 / (2 * (n : ℝ) * ((n : ℝ) + 1)) := by
 116  unfold superparticular Jcost
 117  have hn_ne : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
 118  have hn1_ne : (n : ℝ) + 1 ≠ 0 := by positivity
 119  field_simp [hn_ne, hn1_ne]
 120  ring
 121
 122theorem superparticular_jcost_decreasing (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (h : m < n) :
 123    Jcost (superparticular n) < Jcost (superparticular m) := by
 124  rw [superparticular_jcost m hm, superparticular_jcost n hn]
 125  have hm_pos : (0 : ℝ) < (m : ℝ) := Nat.cast_pos.mpr hm
 126  have hn_pos : (0 : ℝ) < (n : ℝ) := Nat.cast_pos.mpr hn
 127  have hm1_pos : (0 : ℝ) < (m : ℝ) + 1 := by linarith
 128  have hn1_pos : (0 : ℝ) < (n : ℝ) + 1 := by linarith
 129  have h_cast : (m : ℝ) < (n : ℝ) := Nat.cast_lt.mpr h
 130  apply div_lt_div_of_pos_left (by norm_num : (0 : ℝ) < 1)
 131  · positivity
 132  · have : (m : ℝ) * ((m : ℝ) + 1) < (n : ℝ) * ((n : ℝ) + 1) := by nlinarith
 133    linarith
 134
 135/-! ## Consonance as Low J-Cost (no free parameters)
 136
 137The central philosophical point: consonance IS low J-cost.
 138There is no separate "consonance function" — the same cost function
 139that drives all of physics also determines musical beauty. -/
 140
 141theorem consonance_is_jcost (r : ℝ) (hr : 0 < r) :
 142    intervalCost r = 0 ↔ r = 1 := by
 143  unfold intervalCost
 144  exact Jcost_eq_zero_iff r hr
 145
 146theorem dissonance_is_high_jcost (r : ℝ) (hr : 0 < r) (hr1 : r ≠ 1) :
 147    0 < intervalCost r := by
 148  unfold intervalCost
 149  exact Jcost_pos_of_ne_one r hr hr1
 150
 151end IndisputableMonolith.MusicTheory.Consonance
 152