classifyValence

formal source

  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