sigmaCost
plain-language theorem explainer
SigmaCost assigns a real-valued agency imbalance to each trolley choice, returning 1 for the active pull and 0 for do-nothing. Decision theorists resolving Newcomb-style paradoxes under sigma conservation cite it to quantify the J-sigma tradeoff in the classic dilemma. The definition is realized by exhaustive case analysis on the two constructors of TrolleyChoice.
Claim. For a trolley choice $c$, the sigma-cost is defined by $1$ when $c$ is the pull action and $0$ when $c$ is the do-nothing action.
background
TrolleyChoice is the inductive type with constructors pull and doNothing, representing the active intervention versus passive option in the runaway-trolley scenario. Sigma-cost measures the agency imbalance created by a choice, directly analogous to the NewcombParadox.sigmaCost definition that assigns 0 to one-boxing and 1 to two-boxing. Upstream cost functions from MultiplicativeRecognizerL4.cost and ObserverForcing.cost supply the general recognition-cost machinery that this definition specializes to the trolley setting. The module frames the trolley problem as a strict J-sigma tradeoff: pulling reduces lives lost but introduces sigma-skew, while doing nothing preserves sigma at the cost of higher J.
proof idea
The definition is a direct pattern match on the TrolleyChoice constructors, returning the constant 1 for pull and 0 for doNothing.
why it matters
This definition supplies the sigmaCost field required by TrolleyTradeoffCert and is referenced by NewcombResolutionCert, oneBox_dominates_under_sigma_conservation, and related results to establish dominance under sigma conservation. It fills the philosophical-paradoxes row of the Recognition Science framework by quantifying the J-sigma tradeoff, where active killing breaks the no-action equilibrium even while lowering J-cost. The construction connects to the eight-tick octave and RCL through the sigma-conservation enforced by R-hat action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.