livesLost
plain-language theorem explainer
This definition maps each trolley choice to the number of lives lost, returning 1 for pulling the lever and 5 for doing nothing. Ethicists and decision theorists working in the Recognition Science framework cite it to quantify the J-cost axis of the trolley tradeoff. It is realized as a direct pattern match on the inductive TrolleyChoice type.
Claim. The function $livesLost : TrolleyChoice → ℕ$ is given by $livesLost(pull) = 1$ and $livesLost(doNothing) = 5$.
background
The module frames the trolley problem as a J/σ tradeoff inside Recognition Science. TrolleyChoice is the inductive type with constructors pull and doNothing. livesLost supplies the integer count of deaths for each choice and serves as the proxy for J-cost on the lives manifold, where J-cost is the recognition cost derived from the multiplicative recognizer or observer forcing cost functions. The local setting contrasts utilitarian J-minimization (pull saves four lives) against deontological σ-preservation (pull creates an agency imbalance). Upstream results supply the cost definitions: cost from MultiplicativeRecognizerL4 as derivedCost on positive ratios, cost from ObserverForcing as Jcost of the recognition event state, and the from theorem that extracts four structural conditions from seven axioms.
proof idea
The definition is a direct case match on the TrolleyChoice inductive type, returning the literal 1 for the pull constructor and 5 for doNothing.
why it matters
This definition supplies the concrete values that populate jCost, enable the pull_lowers_J theorem, and complete the fields of the TrolleyTradeoffCert structure. It anchors the J-axis of the tradeoff in the trolley problem, where pulling reduces lives lost from 5 to 1 while raising sigmaCost. The result supports the no_strictly_dominant_choice lemma showing that neither option dominates on both axes simultaneously, consistent with the J/σ tension described in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.