pull_lowers_J
plain-language theorem explainer
The declaration establishes that the J-cost of pulling the lever is strictly smaller than the J-cost of inaction, with J-cost defined directly as the number of lives lost. Decision theorists working in the Recognition Science framework would cite it to quantify the utilitarian side of the trolley dilemma. The proof is a term-mode reduction that unfolds the cost definitions and normalizes the resulting numerical inequality.
Claim. Let $jCost(c)$ be the J-cost of choice $c$, defined as the real number of lives lost under $c$. Then $jCost(pull) < jCost(doNothing)$, which evaluates to $1 < 5$.
background
The Trolley module recasts the classic dilemma as a J/σ tradeoff. The inductive type TrolleyChoice has constructors pull and doNothing. livesLost maps pull to 1 and doNothing to 5; jCost is the real-valued lift of livesLost. sigmaCost assigns 1 to pull (agency imbalance) and 0 to doNothing, following the template from NewcombParadox.sigmaCost where one-boxing carries zero σ-cost.
proof idea
The proof is a one-line wrapper that unfolds jCost and livesLost, then applies norm_num to compare the constants 1 and 5.
why it matters
This supplies the J-decrease half of tradeoff_strict, which pairs it with the σ-increase to feed no_strictly_dominant_choice. The module documentation positions the result as realizing the strict J/σ tension in the trolley problem, where pulling lowers J but creates an agency imbalance. It illustrates cost computation on the lives manifold inside the Recognition Science decision layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.