oneBox_dominates_under_sigma_conservation
plain-language theorem explainer
Under the constraint that sigma-cost equals zero for a Newcomb choice, the only admissible option is the one-box choice. Decision theorists working inside Recognition Science frameworks cite this result to dissolve Newcomb's paradox via conservation of the sigma quantity between Z-matched predictor and chooser. The proof is a direct case split on the inductive NewcombChoice type that yields reflexivity on oneBox and an immediate contradiction on twoBox.
Claim. Let $c$ be a Newcomb choice. If the sigma-cost of $c$ equals zero, then $c$ equals the one-box choice.
background
Newcomb's paradox is recast in Recognition Science as a structural theorem about sigma-conservation: a perfect predictor is a Z-matched copy of the chooser, so sigma must be preserved by the R-hat action. The NewcombChoice type is the inductive type with constructors oneBox and twoBox. The sigmaCost function returns zero on oneBox and one on twoBox, measuring the imbalance created when the chooser's action fails to match the predictor's forecast. This theorem depends on the sigmaCost definition in the same module and on the analogous sigmaCost construction in the Trolley module that treats lives lost as a real-valued agency cost.
proof idea
The proof executes case analysis on the NewcombChoice inductive type. The oneBox case is closed by reflexivity. The twoBox case derives a contradiction by rewriting the hypothesis with the definition of sigmaCost, which evaluates to one.
why it matters
This result supplies the one_box_under_constraint field of the master certificate newcombResolutionCert. It completes the structural resolution of Newcomb's paradox as a sigma-conservation theorem in the Recognition Science treatment of philosophical paradoxes. The argument rests on the upstream fact that sigma is conserved under R-hat action between Z-matched copies and feeds directly into the five-field certificate that records one-box preservation of sigma, two-box creation of imbalance, and the ordering of costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.