perfectFifth

formal source

  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
  49  composition_law := True
  50  invariance_law := True
  51  nontrivial_law := by
  52    have hne : octave ≠ (⟨1, one_pos⟩ : FrequencyRatio) := by
  53      intro h
  54      have hv := congrArg Subtype.val h
  55      norm_num [octave] at hv
  56    simp [ratioCost, hne]
  57
  58def music_is_positive_ratio_subrealization : True := trivial
  59
  60noncomputable def music_arith_equiv_logicNat :
  61    (StrictLogicRealization.arith strictMusicRealization).peano.carrier
  62      ≃ ArithmeticFromLogic.LogicNat :=
  63  (StrictLogicRealization.toLightweight strictMusicRealization).orbitEquivLogicNat
  64