TrolleyChoice
plain-language theorem explainer
TrolleyChoice supplies the two-element domain for the trolley problem in Recognition Science, distinguishing the action of pulling the lever from inaction. Modelers of ethical J/σ tradeoffs cite it to anchor cost functions that separate lives-lost minimization from agency-imbalance penalties. The declaration is a direct inductive definition with constructors pull and doNothing, automatically deriving decidable equality and inhabitedness.
Claim. Let $T$ be the set of trolley choices with two elements: pull (diverting the trolley, incurring one death) and doNothing (preserving the original track, incurring five deaths).
background
The module frames the classic trolley dilemma inside Recognition Science as a strict J/σ tradeoff. Utilitarian evaluation tracks J-cost via lives lost; deontological evaluation tracks σ-cost via the agency imbalance created by an active intervention. livesLost maps pull to 1 and doNothing to 5; sigmaCost maps pull to 1 and doNothing to 0; jCost simply lifts livesLost to the reals. The setting sits in the philosophical-paradoxes row of the framework and references the 14 DREAM virtues as the structural bridge that could, in principle, reconcile the two axes.
proof idea
The declaration is an inductive definition that introduces exactly two constructors, pull and doNothing. Derivation of DecidableEq and Inhabited is automatic; no lemmas or tactics are invoked.
why it matters
TrolleyChoice is the root type for every downstream result in the module: jCost, livesLost, sigmaCost, pull_lowers_J, pull_raises_sigma, tradeoff_strict, and no_strictly_dominant_choice all quantify over it. It supplies the concrete instance of the J/σ tradeoff described in the module documentation, placing the trolley problem inside the Recognition Science treatment of ethical decisions. The construction touches the open question whether a virtue-aligned action can ever escape the strict dominance prohibition shown by no_strictly_dominant_choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.