IndisputableMonolith.Decision.Trolley

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# The Trolley Problem as a J/σ Tradeoff
   7
   8## §XXIII.C row "Philosophical paradoxes" — Trolley side.
   9
  10The trolley problem: a runaway trolley will kill 5 people unless
  11diverted onto a side track that will kill 1 person.  Pull the
  12lever to divert (utilitarian) or do nothing (deontological)?
  13
  14In RS: utilitarianism minimizes J-cost (5 lives saved >
  151 life saved).  Deontology preserves σ-conservation: the act of
  16pulling the lever creates a σ-imbalance (an act of agency that
  17breaks the no-action equilibrium), even though it strictly
  18decreases J.
  19
  20The genuine moral tension is the J/σ tradeoff:
  21
  22  - Pulling the lever: J decreases (5 → 1 deaths) but σ-skew
  23    is created (active killing introduces an agency-imbalance).
  24  - Not pulling: σ is preserved but J is maximal.
  25
  26The 14 DREAM virtues from `Ethics/Virtues/CompletenessClosure`
  27provide the structural bridge: a virtue-aligned action can be
  28J-reducing AND σ-preserving simultaneously, but the trolley
  29constraints force a strict tradeoff.
  30
  31## What this module provides
  32
  331. `TrolleyChoice`: inductive `pull | doNothing`.
  342. `livesLost`: 1 (pull) or 5 (doNothing).
  353. `sigmaCost`: 1 (pull, agency imbalance) or 0 (doNothing).
  364. `jCost`: lives lost (proxy for J-cost on the lives manifold).
  375. `tradeoff_strict`: pulling lowers J but raises σ.
  386. `no_strictly_dominant_choice`: neither choice dominates the
  39   other on both axes.
  407. Master cert `TrolleyTradeoffCert` with 5 fields.
  41-/
  42
  43namespace IndisputableMonolith
  44namespace Decision
  45namespace Trolley
  46
  47open Constants
  48
  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
  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
 113  | doNothing =>
 114    cases c2 with
 115    | pull =>
 116      have := pull_lowers_J
 117      linarith
 118    | doNothing => exact absurd rfl h_diff
 119
 120/-! ## Master certificate -/
 121
 122/-- **TROLLEY TRADEOFF MASTER CERTIFICATE.** -/
 123structure TrolleyTradeoffCert where
 124  pull_lives_lost : livesLost TrolleyChoice.pull = 1
 125  doNothing_lives_lost : livesLost TrolleyChoice.doNothing = 5
 126  tradeoff :
 127    jCost TrolleyChoice.pull < jCost TrolleyChoice.doNothing ∧
 128    sigmaCost TrolleyChoice.pull > sigmaCost TrolleyChoice.doNothing
 129  no_dominance :
 130    ∀ (c1 c2 : TrolleyChoice), c1 ≠ c2 →
 131      ¬ (jCost c1 < jCost c2 ∧ sigmaCost c1 < sigmaCost c2)
 132  pull_creates_agency_imbalance :
 133    sigmaCost TrolleyChoice.pull = 1
 134
 135/-- The master certificate is inhabited. -/
 136def trolleyTradeoffCert : TrolleyTradeoffCert where
 137  pull_lives_lost := rfl
 138  doNothing_lives_lost := rfl
 139  tradeoff := tradeoff_strict
 140  no_dominance := no_strictly_dominant_choice
 141  pull_creates_agency_imbalance := rfl
 142
 143end
 144
 145end Trolley
 146end Decision
 147end IndisputableMonolith
 148