`TrolleyChoice`

definition

show as: view math explainer →

module: IndisputableMonolith.Decision.Trolley
domain: Decision
line: 52 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Decision.Trolley on GitHub at line 52.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  49noncomputable section
  50
  51/-- The trolley choice: pull the lever or do nothing. -/
  52inductive TrolleyChoice where
  53  | pull
  54  | doNothing
  55  deriving DecidableEq, Inhabited
  56
  57namespace TrolleyChoice
  58
  59/-- Display name. -/
  60def name : TrolleyChoice → String
  61  | pull      => "pull lever"
  62  | doNothing => "do nothing"
  63
  64end TrolleyChoice
  65
  66/-- Lives lost as a function of choice. -/
  67def livesLost (c : TrolleyChoice) : ℕ :=
  68  match c with
  69  | TrolleyChoice.pull      => 1
  70  | TrolleyChoice.doNothing => 5
  71
  72/-- σ-cost: agency imbalance from active killing. -/
  73def sigmaCost (c : TrolleyChoice) : ℝ :=
  74  match c with
  75  | TrolleyChoice.pull      => 1
  76  | TrolleyChoice.doNothing => 0
  77
  78/-- J-cost proxy: lives lost as real number. -/
  79def jCost (c : TrolleyChoice) : ℝ := (livesLost c : ℝ)
  80
  81/-- Pulling lowers J: `jCost(pull) < jCost(doNothing)`. -/
  82theorem pull_lowers_J : jCost TrolleyChoice.pull < jCost TrolleyChoice.doNothing := by

papers checked against this theorem

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