`narrative_admissible`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.AdmissibleClass
domain: Foundation
line: 71 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.AdmissibleClass on GitHub at line 71.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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
  94version applies `StrictLogicRealization.universal_forcing R S` directly,
  95having confirmed admissibility via the witnesses below. -/
  96
  97/-- Restating the structural fact: admissibility witnesses exist for the
  98    four canonical domain realizations. The actual universal forcing
  99    equivalence is the universally available
 100    `StrictLogicRealization.universal_forcing`, which does not depend on
 101    admissibility. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.