`sigmaCost`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Decision.Trolley on GitHub at line 73.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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
  91
  92/-- The tradeoff is strict: lowering J requires raising σ, and
  93    vice versa. -/
  94theorem tradeoff_strict :
  95    jCost TrolleyChoice.pull < jCost TrolleyChoice.doNothing ∧
  96    sigmaCost TrolleyChoice.pull > sigmaCost TrolleyChoice.doNothing :=
  97  ⟨pull_lowers_J, pull_raises_sigma⟩
  98
  99/-- No choice strictly dominates the other on both axes.
 100    Pulling is better on J, worse on σ; doNothing is the reverse. -/
 101theorem no_strictly_dominant_choice
 102    (c1 c2 : TrolleyChoice)
 103    (h_diff : c1 ≠ c2) :

papers checked against this theorem

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