jCost
plain-language theorem explainer
jCost maps each trolley choice to the real number of lives lost, serving as the J-cost proxy for quantifying the utilitarian side of the pull versus do-nothing dilemma. Decision theorists applying Recognition Science to ethical paradoxes would cite this when comparing J-reduction against sigma-imbalance. The definition is a direct type cast from the integer livesLost function.
Claim. For a choice $c$ in the trolley problem (pull the lever or do nothing), define $jCost(c)$ to be the real number equal to the count of lives lost under $c$.
background
The module treats the trolley problem as a J/σ tradeoff inside Recognition Science. TrolleyChoice is the inductive type whose constructors are pull and doNothing. livesLost returns the natural number 1 for pull and 5 for doNothing; sigmaCost returns the binary agency flag 1 for pull and 0 for doNothing. jCost lifts the livesLost count to ℝ to serve as a proxy for J-cost on the lives manifold, enabling direct numerical comparison with sigmaCost.
proof idea
The definition is a one-line wrapper that applies the cast from livesLost to ℝ.
why it matters
jCost supplies the J-axis for the downstream theorems pull_lowers_J, tradeoff_strict, no_strictly_dominant_choice and the master TrolleyTradeoffCert. It also feeds the PreTemporalForcingOrder lemmas jCost_before_arithmetic and rank, placing this concrete J-cost instance prior to arithmetic stages. Within the RS framework it instantiates the J-uniqueness landmark (T5) for a philosophical paradox, exposing the strict J/σ tension that the 14 DREAM virtues are intended to bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.