biology_admissible

formal source

  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
  85    rfl
  86
  87/-! ## Headline theorem: quantified universal forcing
  88
  89Universal forcing is provided by `StrictLogicRealization.universal_forcing`
  90on the underlying realization pair, regardless of admissibility. The
  91*content* of this module is the existence of `AdmissibleRealization`
  92witnesses for the four canonical domain realizations (Music, Biology,
  93Narrative, Ethics). The downstream consumer wishing the quantified