IndisputableMonolith.Foundation.UniversalForcing.Strict.Music

   1import IndisputableMonolith.Foundation.UniversalForcing.Strict.Invariance
   2
   3/-!
   4  Strict/Music.lean
   5
   6  Domain-rich musical realization over positive frequency ratios.  The
   7  comparison is equality-cost on ratios for this strict pass; richer
   8  psychoacoustic dissonance costs can refine it later.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Foundation
  13namespace UniversalForcing
  14namespace Strict
  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
  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
  65end Music
  66end Strict
  67end UniversalForcing
  68end Foundation
  69end IndisputableMonolith
  70