IndisputableMonolith.MusicTheory.Valence

   1/-
   2  MusicTheory/Valence.lean
   3
   4  MAJOR/MINOR VALENCE FROM LEDGER SKEW
   5
   6  Why does a major chord sound "bright" and a minor chord sound "dark"?
   7  In RS, the ledger skew σ determines hedonic valence. A musical interval
   8  has an intrinsic asymmetry (r ≠ 1/r for r ≠ 1), and this asymmetry
   9  is precisely the ledger skew induced by the interval.
  10
  11  The major third (5/4) has higher skew than the minor third (6/5),
  12  which maps to positive vs. negative valence — brightness vs. darkness.
  13
  14  Part of: IndisputableMonolith/MusicTheory/
  15-/
  16
  17import Mathlib
  18import IndisputableMonolith.MusicTheory.HarmonicModes
  19
  20namespace IndisputableMonolith.MusicTheory.Valence
  21
  22/-! ## Ledger Skew of an Interval
  23
  24The asymmetry of ratio r is r - 1/r. For r > 1 this is positive,
  25measuring how far r deviates from reciprocal symmetry.
  26Larger skew = more expansive = brighter valence. -/
  27
  28@[simp] noncomputable def majorThird : ℝ := 5 / 4
  29@[simp] noncomputable def minorThird : ℝ := 6 / 5
  30
  31noncomputable def ledgerSkew (r : ℝ) : ℝ := r - r⁻¹
  32
  33theorem ledgerSkew_zero_at_unity : ledgerSkew 1 = 0 := by
  34  simp [ledgerSkew]
  35
  36theorem ledgerSkew_pos_above_one (r : ℝ) (hr : 1 < r) :
  37    0 < ledgerSkew r := by
  38  unfold ledgerSkew
  39  have hr_pos : 0 < r := by linarith
  40  have hr_inv_lt : r⁻¹ < 1 := inv_lt_one_of_one_lt₀ hr
  41  linarith
  42
  43theorem ledgerSkew_neg_below_one (r : ℝ) (hr_pos : 0 < r) (hr_lt : r < 1) :
  44    ledgerSkew r < 0 := by
  45  unfold ledgerSkew
  46  have hr_inv_gt : 1 < r⁻¹ := (one_lt_inv₀ hr_pos).2 hr_lt
  47  linarith
  48
  49theorem ledgerSkew_antisymmetric (r : ℝ) (_hr : r ≠ 0) :
  50    ledgerSkew r⁻¹ = -ledgerSkew r := by
  51  unfold ledgerSkew
  52  rw [inv_inv]
  53  ring
  54
  55/-! ## Major vs Minor Skew -/
  56
  57theorem major_third_skew :
  58    ledgerSkew majorThird = 9 / 20 := by
  59  simp [ledgerSkew]; ring
  60
  61theorem minor_third_skew :
  62    ledgerSkew minorThird = 11 / 30 := by
  63  simp [ledgerSkew]; ring
  64
  65theorem major_third_skew_pos :
  66    0 < ledgerSkew majorThird := by
  67  rw [major_third_skew]
  68  norm_num
  69
  70theorem minor_third_skew_pos :
  71    0 < ledgerSkew minorThird := by
  72  rw [minor_third_skew]
  73  norm_num
  74
  75theorem major_skew_gt_minor_skew :
  76    ledgerSkew majorThird > ledgerSkew minorThird := by
  77  rw [major_third_skew, minor_third_skew]; norm_num
  78
  79/-! ## Valence Classification -/
  80
  81inductive Valence
  82  | positive
  83  | negative
  84  | neutral
  85  deriving DecidableEq, Repr
  86
  87noncomputable def classifyValence (r : ℝ) (threshold : ℝ) : Valence :=
  88  if ledgerSkew r > threshold then .positive
  89  else if ledgerSkew r < -threshold then .negative
  90  else .neutral
  91
  92theorem major_is_positive :
  93    classifyValence majorThird 0 = .positive := by
  94  unfold classifyValence
  95  rw [major_third_skew]
  96  norm_num
  97
  98theorem minor_is_positive_but_less :
  99    classifyValence minorThird 0 = .positive := by
 100  unfold classifyValence
 101  rw [minor_third_skew]
 102  norm_num
 103
 104/-! ## Why Music Moves Us
 105
 106The skew difference between major and minor thirds IS the valence
 107difference experienced by the listener. Music literally modulates
 108the ledger skew σ, and σ IS hedonic experience. -/
 109
 110theorem valence_difference :
 111    ledgerSkew majorThird - ledgerSkew minorThird = 5 / 60 := by
 112  rw [major_third_skew, minor_third_skew]; norm_num
 113
 114theorem valence_difference_one_twelfth :
 115    ledgerSkew majorThird - ledgerSkew minorThird = 1 / 12 := by
 116  rw [valence_difference]
 117  norm_num
 118
 119theorem skew_increases_with_interval_size (r₁ r₂ : ℝ)
 120    (h1 : 1 < r₁) (_h2 : 1 < r₂) (h : r₁ < r₂)
 121    (_hr1_lt_2 : r₁ < 2) (_hr2_lt_2 : r₂ < 2) :
 122    ledgerSkew r₁ < ledgerSkew r₂ := by
 123  unfold ledgerSkew
 124  have hr1_pos : 0 < r₁ := by linarith
 125  have hr2_pos : 0 < r₂ := by linarith
 126  have h_inv : r₂⁻¹ < r₁⁻¹ := by
 127    simp only [inv_eq_one_div]
 128    exact one_div_lt_one_div_of_lt hr1_pos h
 129  linarith
 130
 131end IndisputableMonolith.MusicTheory.Valence
 132