pull_raises_sigma
The declaration proves that diverting the trolley raises the agency-imbalance cost relative to inaction. Decision theorists applying Recognition Science to moral dilemmas cite it to establish the strict J/σ tradeoff. The proof is a one-line wrapper that unfolds the sigmaCost definition and normalizes the constants.
claimLet $T$ be the inductive type with constructors pull and doNothing. Let $σ : T → ℝ$ be defined by $σ(pull) = 1$ and $σ(doNothing) = 0$. Then $σ(pull) > σ(doNothing)$.
background
The Decision.Trolley module recasts the classic trolley problem as a J/σ tradeoff inside Recognition Science. TrolleyChoice is the inductive type with constructors pull (active diversion) and doNothing (inaction). The function sigmaCost assigns the real value 1 to pull, reflecting the agency imbalance created by intervention, and 0 to doNothing, as stated in its sibling definition. This construction mirrors the sigmaCost pattern already introduced in NewcombParadox for predictor scenarios.
proof idea
The proof is a one-line wrapper. It unfolds sigmaCost on both constructors and applies norm_num to verify the numerical comparison 1 > 0.
why it matters in Recognition Science
The result is used by tradeoff_strict to package the opposing movements on the two axes and by no_strictly_dominant_choice to show that neither option dominates both metrics simultaneously. It supplies the σ-raising half of the trolley instance of the J/σ tradeoff described in the module's treatment of philosophical paradoxes. The strict inequality highlights why the 14 DREAM virtues are invoked elsewhere to seek resolutions that avoid the forced tradeoff.
scope and limits
- Does not resolve the underlying moral dilemma.
- Does not model probabilistic outcomes or continuous choices.
- Does not incorporate the 14 DREAM virtues.
- Does not generalize the cost functions beyond the two discrete options.
Lean usage
theorem example : jCost TrolleyChoice.pull < jCost TrolleyChoice.doNothing ∧ sigmaCost TrolleyChoice.pull > sigmaCost TrolleyChoice.doNothing := ⟨pull_lowers_J, pull_raises_sigma⟩formal statement (Lean)
87theorem pull_raises_sigma :
88 sigmaCost TrolleyChoice.pull > sigmaCost TrolleyChoice.doNothing := by
proof body
Term-mode proof.
89 unfold sigmaCost
90 norm_num
91
92/-- The tradeoff is strict: lowering J requires raising σ, and
93 vice versa. -/