AdmissibleRealization

formal source

  39
  40/-- A strict realization is *admissible* when it satisfies non-trivial
  41    structural laws on top of the basic identity / non-contradiction. -/
  42structure AdmissibleRealization (R : StrictLogicRealization) where
  43  /-- Cost equality is decidable (excluded middle on the cost predicate). -/
  44  cost_decidable : ∀ x y : R.Carrier, Decidable (R.compare x y = 0)
  45  /-- Composition is associative. -/
  46  compose_assoc : ∀ a b c : R.Carrier,
  47      R.compose (R.compose a b) c = R.compose a (R.compose b c)
  48  /-- The chosen `one` is a left identity (or analog). -/
  49  compose_one_or_step : R.compose R.one R.one = R.one ∨
  50                        R.compose R.one R.generator = R.generator
  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 ?_⟩