`strictEthicsRealization`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.Strict.Ethics
domain: Foundation
line: 42 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.Strict.Ethics on GitHub at line 42.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  39def minimalImprovement : ActionState := ⟨0, 1⟩
  40
  41/-- Strict ethical realization using minimal improvement as generator. -/
  42def strictEthicsRealization : StrictLogicRealization where
  43  Carrier := ActionState
  44  Cost := Nat
  45  zeroCost := inferInstance
  46  compare := actionCost
  47  compose := preferenceCompose
  48  one := ethicalZero
  49  generator := minimalImprovement
  50  identity_law := actionCost_self
  51  non_contradiction_law := actionCost_symm
  52  excluded_middle_law := True
  53  composition_law := True
  54  invariance_law := True
  55  nontrivial_law := by
  56    simp [actionCost, minimalImprovement, ethicalZero]
  57
  58def ethics_arith_equiv_logicNat :
  59    (StrictLogicRealization.arith strictEthicsRealization).peano.carrier
  60      ≃ ArithmeticFromLogic.LogicNat :=
  61  (StrictLogicRealization.toLightweight strictEthicsRealization).orbitEquivLogicNat
  62
  63end Ethics
  64end Strict
  65end UniversalForcing
  66end Foundation
  67end IndisputableMonolith

papers checked against this theorem

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