tradeoff_strict
plain-language theorem explainer
In the trolley problem formalized in Recognition Science, the pull choice yields strictly lower J-cost than doNothing while producing strictly higher σ-cost. Decision theorists examining ethical paradoxes would cite this to quantify the tension between lives-lost minimization and agency preservation. The proof is a direct term that conjoins the two component lemmas establishing each inequality separately.
Claim. Let $jCost$ be the real-valued proxy for J-cost given by lives lost and let $sigmaCost$ be the real-valued measure of σ-cost given by agency imbalance. Then $jCost(pull) < jCost(doNothing) ∧ sigmaCost(pull) > sigmaCost(doNothing)$.
background
The module treats the trolley problem as a J/σ tradeoff inside the Recognition Science treatment of philosophical paradoxes. TrolleyChoice is the inductive type whose constructors are pull and doNothing. The definition jCost maps each choice to the corresponding number of lives lost (1 for pull, 5 for doNothing). The definition sigmaCost assigns 1 to pull, recording the agency imbalance introduced by active intervention, and 0 to doNothing.
proof idea
The proof is the term that directly pairs the upstream lemmas pull_lowers_J and pull_raises_sigma to inhabit the conjunction.
why it matters
The theorem supplies the tradeoff field inside the master certificate trolleyTradeoffCert. It completes the formalization of the trolley problem as a strict J/σ tradeoff, showing that the constraints prevent simultaneous optimization on both axes even though the 14 DREAM virtues can in principle bridge them. The result sits inside the Decision domain and illustrates how Recognition Science encodes the utilitarian-deontological tension via the J-cost and σ-cost functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.