NewcombResolutionCert
plain-language theorem explainer
NewcombResolutionCert packages five properties establishing that one-boxing incurs zero σ-cost while two-boxing incurs unit cost, that the zero-cost choice is unique, and that one-boxing dominates by 999000 under perfect prediction. Decision theorists working inside Recognition Science cite it to treat Newcomb's paradox as a σ-conservation theorem rather than a split between causal and evidential reasoning. The declaration is a structure definition that directly records the five properties drawn from sibling sigmaCost and expectedValue lemmas.
Claim. Let σ denote the σ-cost of a choice when paired with a perfect predictor. The certificate certifies σ(one-box strategy) = 0, σ(two-box strategy) = 1, σ(one-box) < σ(two-box), that the one-box strategy is the unique choice with σ-cost zero, and that the expected-value gap under perfect prediction equals 999000.
background
The module treats Newcomb's paradox inside Recognition Science as a σ-conservation theorem. NewcombChoice is the inductive type with constructors oneBox (take only Box B) and twoBox (take both boxes). The function expectedValue computes standard expected payoff assuming the predictor matches the choice with probability p; at p = 1 it returns 1000000 for oneBox and 1001000 for twoBox. The function sigmaCost assigns 0 to oneBox and 1 to twoBox, measuring the imbalance between prediction and action as a J-cost proxy.
proof idea
As a structure definition the declaration directly assembles the five fields. The first two fields are the direct evaluations of sigmaCost on each constructor. The ordering field is the strict inequality between those values. The constraint field is the universal statement that zero σ-cost forces the oneBox constructor. The dominance field is the numerical subtraction of the two expectedValue calls at p = 1.
why it matters
The structure is instantiated by the downstream definition newcombResolutionCert, which populates each field from sibling lemmas such as oneBox_preserves_sigma and oneBox_dominates_at_perfect_prediction. It completes the Newcomb side of the philosophical-paradoxes row in §XXIII.C by showing the paradox dissolves once σ-conservation between predictor and agent is required. In the larger framework it aligns with the Recognition Composition Law by treating any prediction-action mismatch as a positive defect cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.