FrequencyRatio

formal source

  15namespace Music
  16
  17/-- Positive frequency ratio. -/
  18abbrev FrequencyRatio := {x : ℝ // 0 < x}
  19
  20noncomputable def ratioCost (a b : FrequencyRatio) : Nat :=
  21  if a = b then 0 else 1
  22
  23@[simp] theorem ratioCost_self (a : FrequencyRatio) : ratioCost a a = 0 := by
  24  simp [ratioCost]
  25
  26theorem ratioCost_symm (a b : FrequencyRatio) : ratioCost a b = ratioCost b a := by
  27  by_cases h : a = b
  28  · subst h
  29    simp [ratioCost]
  30  · have h' : b ≠ a := by intro hb; exact h hb.symm
  31    simp [ratioCost, h, h']
  32
  33def octave : FrequencyRatio := ⟨2, by norm_num⟩
  34noncomputable def perfectFifth : FrequencyRatio := ⟨(3 : ℝ) / 2, by norm_num⟩
  35noncomputable def perfectFourth : FrequencyRatio := ⟨(4 : ℝ) / 3, by norm_num⟩
  36
  37/-- Strict musical realization using octave stacking as the canonical generator. -/
  38noncomputable def strictMusicRealization : StrictLogicRealization where
  39  Carrier := FrequencyRatio
  40  Cost := Nat
  41  zeroCost := inferInstance
  42  compare := ratioCost
  43  compose := fun a b => ⟨a.1 * b.1, mul_pos a.2 b.2⟩
  44  one := ⟨1, one_pos⟩
  45  generator := octave
  46  identity_law := ratioCost_self
  47  non_contradiction_law := ratioCost_symm
  48  excluded_middle_law := True