`pull_lowers_J`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Decision.Trolley on GitHub at line 82.

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

  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) :
 104    ¬ (jCost c1 < jCost c2 ∧ sigmaCost c1 < sigmaCost c2) := by
 105  intro ⟨hJ, hσ⟩
 106  cases c1 with
 107  | pull =>
 108    cases c2 with
 109    | pull => exact absurd rfl h_diff
 110    | doNothing =>
 111      have := pull_raises_sigma
 112      linarith

papers checked against this theorem

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