sigmaCost_ordering
plain-language theorem explainer
The theorem shows that the sigma-cost assigned to one-boxing is strictly smaller than the sigma-cost assigned to two-boxing. Decision theorists citing the Recognition Science treatment of Newcomb's paradox use this ordering to establish that one-boxing is the unique sigma-conserving choice. The proof is a one-line wrapper that unfolds the sigmaCost definition and normalizes the resulting constants.
Claim. Let the sigma-cost function assign the value 0 to the one-box choice and the value 1 to the two-box choice. Then the sigma-cost of one-boxing is strictly less than the sigma-cost of two-boxing: $0 < 1$.
background
Newcomb's paradox is recast in the module as a sigma-conservation theorem. A perfect predictor is treated as a Z-matched copy of the chooser, so that sigma becomes a conserved quantity under the R-hat action. The sigmaCost definition supplies the concrete values: it returns 0 on the oneBox constructor and 1 on the twoBox constructor. This ordering is one of five fields required by the master NewcombResolutionCert certificate.
proof idea
The proof is a one-line wrapper. It unfolds the sigmaCost definition, which replaces each choice constructor by its numeric value, then applies norm_num to obtain the inequality 0 < 1.
why it matters
The result supplies the sigma-ordering field inside newcombResolutionCert, the master certificate that closes the Newcomb resolution. It thereby places the paradox inside the Recognition Science treatment of philosophical paradoxes, where sigma-conservation replaces the classical causal-evidential split. The ordering is cited by any downstream argument that invokes oneBox_dominates_under_sigma_conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.