IndisputableMonolith.Decision.Trolley
The Decision.Trolley module encodes the trolley problem as a binary choice between pulling the lever and doing nothing, equipped with lives-lost counts and RS-native sigma and J costs. Decision theorists working in Recognition Science would cite it when applying cost functions to ethical dilemmas. The module supplies definitions plus short lemmas that establish a strict tradeoff and certify the absence of a dominant option.
claim$TrolleyChoice := pull | doNothing$, with $livesLost : TrolleyChoice → ℕ$, $sigmaCost$ and $jCost$ drawn from the Cost module, satisfying $pull_lowers_J$, $pull_raises_sigma$, $tradeoff_strict$, and $no_strictly_dominant_choice$, certified by $TrolleyTradeoffCert$.
background
The module sits in the Decision domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the cost primitives defined in the Cost module. It introduces TrolleyChoice as the two-option decision and attaches the functions livesLost, sigmaCost, and jCost to each option. The imported cost structures supply the J-cost and sigma-cost measures used throughout the subsequent lemmas.
proof idea
The module first declares the TrolleyChoice type and the three cost functions, then proves the four lemmas pull_lowers_J, pull_raises_sigma, tradeoff_strict, and no_strictly_dominant_choice by direct appeal to the definitions imported from Cost. These lemmas are assembled into the certifying object TrolleyTradeoffCert.
why it matters in Recognition Science
The module supplies the trolley-problem instance required by any RS-based decision framework that must handle discrete moral tradeoffs. It demonstrates that the J-cost and sigma-cost pair produces a strict tradeoff with no dominant choice, consistent with the Recognition Composition Law and the cost-minimization principle of the parent framework. No downstream declarations are recorded, so the module functions as a self-contained example or interface for further decision-theoretic extensions.
scope and limits
- Does not assign moral weights beyond the RS cost pair.
- Does not incorporate continuous time or additional physical variables.
- Does not prove that one choice is optimal under any external criterion.
- Does not connect the costs to constants such as alpha or phi.