valence_difference

formal source

 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