79noncomputable def ethics_admissible : AdmissibleRealization Ethics.strictEthicsRealization := by
proof body
Definition body.
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. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.