sigmaCost
plain-language theorem explainer
sigmaCost assigns zero to the one-box choice and one to the two-box choice, quantifying the σ-imbalance created against a perfect predictor. Decision theorists resolving Newcomb's paradox inside Recognition Science cite this definition to ground the claim that one-boxing alone conserves σ. The definition is realized by direct case analysis on the two constructors of NewcombChoice.
Claim. Define the function σ on Newcomb choices by σ(oneBox) = 0 and σ(twoBox) = 1, where oneBox and twoBox are the constructors of the NewcombChoice type.
background
NewcombChoice is the inductive type whose constructors distinguish the one-box strategy (take only the opaque box) from the two-box strategy (take both). sigmaCost supplies the real-valued σ-cost of each choice when the predictor is perfect, returning zero for the coupling-preserving option and one for the coupling-breaking option. This mirrors the sigmaCost definition in the Trolley module, which likewise assigns unit cost to the active choice and zero to the passive choice.
proof idea
The definition proceeds by pattern matching on the NewcombChoice constructors and returns the literal constants 0 and 1. No lemmas or tactics are invoked; the body directly encodes the module's assignment of σ-cost values.
why it matters
sigmaCost supplies the concrete values required by the NewcombResolutionCert structure and by the theorems oneBox_preserves_sigma, twoBox_creates_sigma_imbalance, and sigmaCost_ordering. It thereby completes the σ-conservation resolution of Newcomb's paradox in the philosophical-paradoxes row of the Recognition Science framework, instantiating the Recognition Composition Law in the decision domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.