`PreferLex`

definition

show as: view math explainer →

module: IndisputableMonolith.Ethics.CostModel
domain: Ethics
line: 87 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Ethics.CostModel on GitHub at line 87.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  84  simp [hcost]
  85
  86/-- Lexicographic ethical preference with admissibility first, then cost preference. -/
  87def PreferLex (M : CostModel A) (period : Nat) (cq : CQ)
  88  (hasExpA hasExpB : Prop) (a b : A) : Prop :=
  89  (Admissible period cq hasExpA ∧ ¬ Admissible period cq hasExpB)
  90  ∨ (Admissible period cq hasExpA ∧ Admissible period cq hasExpB ∧ Prefer M a b)
  91
  92end
  93
  94end Ethics
  95end IndisputableMonolith

papers checked against this theorem

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