TrolleyTradeoffCert
plain-language theorem explainer
TrolleyTradeoffCert is a structure that records the strict J-cost versus sigma-cost tension for the trolley problem. Decision theorists working inside Recognition Science cite it when instantiating the master certificate for ethical paradoxes. The definition assembles five fields directly from the lives-lost map, the J-cost proxy, and the sigma-cost assignment.
Claim. A structure whose fields assert lives lost under pull equals 1, lives lost under do-nothing equals 5, J(pull) < J(do-nothing) and sigma(pull) > sigma(do-nothing), no distinct choices c1 and c2 satisfy both J(c1) < J(c2) and sigma(c1) < sigma(c2), and sigma(pull) equals 1.
background
The Decision module recasts the trolley problem as a J/sigma tradeoff. J-cost is the real-valued proxy given by lives lost, while sigma-cost registers the agency imbalance created by an active intervention. The module imports the sigmaCost definition from the Newcomb paradox treatment, where it likewise tracks predictor-related imbalance, and re-uses the same name for the trolley case with values 1 for pull and 0 for inaction.
proof idea
This is a structure definition. Its five fields are populated by direct references to the sibling definitions livesLost, jCost, sigmaCost together with the lemmas tradeoff_strict and no_strictly_dominant_choice.
why it matters
The structure supplies the master certificate for the trolley tradeoff and is inhabited by the definition trolleyTradeoffCert. It occupies the philosophical paradoxes slot in the Decision domain, illustrating the forced J/sigma tension once agency is introduced. The construction closes the scaffolding for ethical decision examples under the Recognition Science treatment of cost and conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.