music_admissible

formal source

  51
  52/-! ## Admissibility for the existing five domain realizations -/
  53
  54noncomputable def music_admissible : AdmissibleRealization Music.strictMusicRealization := by
  55  refine ⟨?_, ?_, Or.inl ?_⟩
  56  · intro a b
  57    apply Classical.dec
  58  · exact RichDomainCosts.MusicRich.compose_assoc
  59  · -- compose one one = one for Music: 1 * 1 = 1
  60    show (⟨(1 : ℝ) * 1, _⟩ : Music.FrequencyRatio) = ⟨1, _⟩
  61    apply Subtype.ext; norm_num
  62
  63noncomputable def biology_admissible : AdmissibleRealization Biology.strictBiologyRealization := by
  64  refine ⟨?_, ?_, Or.inl ?_⟩
  65  · intro a b; exact decEq (Biology.lineageCost a b) 0
  66  · exact RichDomainCosts.BiologyRich.reproduce_assoc
  67  · -- reproduce zero zero = zero
  68    show Biology.reproduce Biology.lineageZero Biology.lineageZero = Biology.lineageZero
  69    rfl
  70
  71noncomputable def narrative_admissible : AdmissibleRealization Narrative.strictNarrativeRealization := by
  72  refine ⟨?_, ?_, Or.inl ?_⟩
  73  · intro a b; exact decEq (Narrative.eventCost a b) 0
  74  · exact RichDomainCosts.NarrativeRich.eventCompose_assoc
  75  · show Narrative.eventCompose Narrative.narrativeZero Narrative.narrativeZero
  76        = Narrative.narrativeZero
  77    rfl
  78
  79noncomputable def ethics_admissible : AdmissibleRealization Ethics.strictEthicsRealization := by
  80  refine ⟨?_, ?_, Or.inl ?_⟩
  81  · intro a b; exact decEq (Ethics.actionCost a b) 0
  82  · exact RichDomainCosts.EthicsRich.preferenceCompose_assoc
  83  · show Ethics.preferenceCompose Ethics.ethicalZero Ethics.ethicalZero
  84        = Ethics.ethicalZero