oneBox_preserves_sigma
plain-language theorem explainer
The declaration shows that the one-box choice in Newcomb's paradox incurs zero sigma-cost under a perfect predictor. Decision theorists working inside the Recognition Science framework cite it when treating the paradox as a structural conservation result rather than a clash between causal and evidential reasoning. The proof is a direct reflexivity reduction from the definition of sigmaCost on the oneBox constructor.
Claim. Let $NewcombChoice$ be the inductive type with constructors $oneBox$ and $twoBox$. Let $sigmaCost$ be the function that returns $0$ on $oneBox$ and $1$ on $twoBox$. Then $sigmaCost(oneBox) = 0$.
background
The Newcomb module treats Newcomb's paradox as a sigma-conservation theorem. NewcombChoice is the inductive type whose constructors distinguish the one-box strategy (take only the opaque box) from the two-box strategy (take both). The sigmaCost function on this type measures the imbalance that arises when an agent's action fails to match a perfect predictor's forecast; it is defined by direct pattern match returning zero for oneBox and one for twoBox. This local setting is embedded in the larger Recognition Science treatment of philosophical paradoxes, where a perfect predictor counts as a Z-matched copy and sigma-cost tracks the resulting recognition defect.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of sigmaCost, which matches the oneBox constructor directly to the value zero.
why it matters
This theorem supplies the first field of the NewcombResolutionCert, the master certificate that assembles the full resolution of the paradox under sigma-conservation. It occupies the Newcomb side of the philosophical-paradoxes row in the Recognition Science framework, confirming that one-boxing is the sigma-preserving choice when predictor-action coupling is required. The result rests on the sigma-cost concept imported from ObserverForcing and MultiplicativeRecognizerL4, where cost is identified with J-cost of recognition events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.