jCost
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive J-cost from the Recognition Composition Law.
- Does not assign continuous or probabilistic values to lives lost.
- Does not prove existence of a virtue-aligned action that eliminates the tradeoff.
- Does not extend the proxy beyond the two discrete choices.
formal statement (Lean)
79def jCost (c : TrolleyChoice) : ℝ := (livesLost c : ℝ)
proof body
Definition body.
80
81/-- Pulling lowers J: `jCost(pull) < jCost(doNothing)`. -/