IndisputableMonolith.Decision.NewcombParadox
The NewcombParadox module encodes Newcomb's paradox in Recognition Science by defining one-box and two-box choices together with their expected values and sigma costs. Decision theorists and foundational physicists cite it for showing one-box dominance when sigma is conserved. The module proceeds via successive definitions of choice, cost ordering, and a final resolution certificate.
claimNewcomb's choice is the selection between one-boxing (opaque box only) and two-boxing (both boxes), resolved by the statement that one-boxing dominates under sigma-cost conservation when prediction is perfect.
background
Recognition Science analyzes decisions through cost functions built from the J-function and the Recognition Composition Law. The module imports the RS time quantum τ₀ = 1 tick from Constants and the cost primitives from the Cost module. It introduces sigmaCost to measure decision imbalance in the Newcomb setup, where perfect prediction is assumed for the dominance arguments.
proof idea
This is a definition module. It first declares NewcombChoice and expectedValue, then defines sigmaCost and its ordering. Lemmas establish that one-boxing preserves sigma while two-boxing creates imbalance, ending with the resolution certificate.
why it matters in Recognition Science
The module supplies an RS-native resolution to Newcomb's paradox and illustrates how cost structures extend the framework to decision problems. It links to the phi-ladder through sigma ordering but lists no downstream theorems.
scope and limits
- Does not model imperfect prediction accuracy.
- Does not derive predictor behavior from RS constants.
- Does not address multi-agent or causal variants.
- Does not compute explicit numerical sigma values.
depends on (2)
declarations in this module (11)
-
inductive
NewcombChoice -
def
name -
def
expectedValue -
theorem
oneBox_dominates_at_perfect_prediction -
def
sigmaCost -
theorem
oneBox_preserves_sigma -
theorem
twoBox_creates_sigma_imbalance -
theorem
sigmaCost_ordering -
theorem
oneBox_dominates_under_sigma_conservation -
structure
NewcombResolutionCert -
def
newcombResolutionCert