twoBox_creates_sigma_imbalance
plain-language theorem explainer
Selecting both boxes in Newcomb's setup produces unit sigma-cost and severs the coupling between a perfect predictor and the agent's action. Decision theorists in the Recognition Science framework cite the result when establishing that one-boxing alone conserves sigma. The proof is a direct reflexivity reduction on the sigmaCost definition for the twoBox constructor.
Claim. The sigma-cost of the two-box choice equals 1.
background
The module recasts Newcomb's paradox as a sigma-conservation theorem inside Recognition Science. NewcombChoice is the inductive type with constructors oneBox and twoBox. sigmaCost is defined by case analysis on this type, returning 0 for oneBox and 1 for twoBox; the value 1 quantifies the imbalance that arises when the agent's action fails to match the predictor's forecast. This definition draws on the general cost functions supplied by MultiplicativeRecognizerL4.cost (derivedCost on positive ratios) and ObserverForcing.cost (J-cost of a recognition event).
proof idea
One-line wrapper that applies reflexivity to the sigmaCost definition for the twoBox case.
why it matters
The theorem supplies the two_box_breaks_sigma field of newcombResolutionCert, the master certificate that certifies one-boxing as the sigma-conserving optimum. It completes the Newcomb side of the philosophical-paradoxes row in the RS framework, linking directly to sigma-conservation between predictor and agent. The result rests on the same cost machinery used for trolley problems and recognition events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.