`ethics_admissible`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

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

  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. -/
 102theorem four_canonical_domains_admissible :
 103    Nonempty (AdmissibleRealization Music.strictMusicRealization) ∧
 104    Nonempty (AdmissibleRealization Biology.strictBiologyRealization) ∧
 105    Nonempty (AdmissibleRealization Narrative.strictNarrativeRealization) ∧
 106    Nonempty (AdmissibleRealization Ethics.strictEthicsRealization) :=
 107  ⟨⟨music_admissible⟩, ⟨biology_admissible⟩,
 108   ⟨narrative_admissible⟩, ⟨ethics_admissible⟩⟩
 109

papers checked against this theorem

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