`name`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Decision.Trolley on GitHub at line 60.

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

  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
  83  unfold jCost livesLost
  84  norm_num
  85
  86/-- Pulling raises σ: `sigmaCost(pull) > sigmaCost(doNothing)`. -/
  87theorem pull_raises_sigma :
  88    sigmaCost TrolleyChoice.pull > sigmaCost TrolleyChoice.doNothing := by
  89  unfold sigmaCost
  90  norm_num

papers checked against this theorem

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