majorThird

formal source

  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