IndisputableMonolith.Decision.NewcombParadox

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Newcomb's Paradox as a σ-Conservation Theorem
   7
   8## §XXIII.C row "Philosophical paradoxes" — Newcomb side.
   9
  10Newcomb's paradox: a perfect predictor offers two boxes.  Box A
  11contains $1000.  Box B contains either $1,000,000 (if predictor
  12predicted you'd take only B) or nothing (otherwise).  Two-box
  13strategy: always take both boxes.  One-box strategy: always take
  14only B.  Classical decision theory splits between causal (two-box)
  15and evidential (one-box) reasoning.
  16
  17In RS, the paradox dissolves: a perfect predictor is, by RS
  18standards, a `Z`-matched copy of the chooser (`p_match(0) = 1`
  19from `ZPatternSoul`).  Two-boxing breaks σ-conservation between
  20the predictor's prediction and the chooser's action — it requires
  21creating a σ-imbalance equal to the prediction error.  One-boxing
  22preserves σ.  Therefore the σ-conserving choice is one-box, and
  23the paradox is resolved as a structural theorem.
  24
  25## What this module provides
  26
  271. `NewcombChoice`: the inductive type `oneBox | twoBox`.
  282. `expectedValue`: standard expected-value computation.
  293. `sigmaCost`: the σ-cost of breaking predictor-action coupling.
  304. `oneBox_preserves_sigma`: one-box is σ-conserving.
  315. `twoBox_creates_sigma_imbalance`: two-box creates σ-imbalance.
  326. `oneBox_dominates_under_sigma_conservation`: one-box is the
  33   structural-theorem optimum when σ-conservation is required.
  347. Master cert `NewcombResolutionCert` with 5 fields.
  35-/
  36
  37namespace IndisputableMonolith
  38namespace Decision
  39namespace NewcombParadox
  40
  41open Constants
  42
  43noncomputable section
  44
  45/-- Newcomb's choice: take both boxes or take only Box B. -/
  46inductive NewcombChoice where
  47  | oneBox
  48  | twoBox
  49  deriving DecidableEq, Inhabited
  50
  51namespace NewcombChoice
  52
  53/-- Display name. -/
  54def name : NewcombChoice → String
  55  | oneBox => "one-box"
  56  | twoBox => "two-box"
  57
  58end NewcombChoice
  59
  60/-- Standard expected value: assumes the predictor is correct
  61    with probability `p` and `1 − p` otherwise.  At `p = 1`
  62    (perfect predictor), one-box wins by `999,000`. -/
  63def expectedValue (c : NewcombChoice) (p : ℝ) : ℝ :=
  64  match c with
  65  | NewcombChoice.oneBox => p * 1000000 + (1 - p) * 0
  66  | NewcombChoice.twoBox => p * 1000 + (1 - p) * 1001000
  67
  68/-- At `p = 1` (perfect predictor), one-box gives 1,000,000 and
  69    two-box gives 1,000.  One-box dominates by 999,000. -/
  70theorem oneBox_dominates_at_perfect_prediction :
  71    expectedValue NewcombChoice.oneBox 1 - expectedValue NewcombChoice.twoBox 1
  72      = 999000 := by
  73  unfold expectedValue
  74  ring
  75
  76/-! ## σ-cost of choice
  77
  78Two-boxing breaks the σ-conservation between the predictor and
  79the chooser: the predictor's σ-skew records "you take one box,"
  80but the chooser's action records "you take two."  The skew
  81mismatch is the σ-cost of breaking coupling.
  82-/
  83
  84/-- The σ-cost of a choice when paired with a perfect predictor. -/
  85def sigmaCost (c : NewcombChoice) : ℝ :=
  86  match c with
  87  | NewcombChoice.oneBox => 0
  88  | NewcombChoice.twoBox => 1
  89
  90/-- One-box has zero σ-cost. -/
  91theorem oneBox_preserves_sigma : sigmaCost NewcombChoice.oneBox = 0 := rfl
  92
  93/-- Two-box has unit σ-cost (breaking predictor-action coupling). -/
  94theorem twoBox_creates_sigma_imbalance :
  95    sigmaCost NewcombChoice.twoBox = 1 := rfl
  96
  97/-- σ-cost ordering: `oneBox < twoBox`. -/
  98theorem sigmaCost_ordering :
  99    sigmaCost NewcombChoice.oneBox < sigmaCost NewcombChoice.twoBox := by
 100  unfold sigmaCost; norm_num
 101
 102/-! ## Resolution: one-box under σ-conservation -/
 103
 104/-- The structural-theorem resolution: under the constraint that
 105    σ-conservation must hold (the predictor and chooser are
 106    Z-matched copies, so σ is a conserved quantity by `R̂`-action),
 107    the unique admissible choice is one-box. -/
 108theorem oneBox_dominates_under_sigma_conservation
 109    (c : NewcombChoice) (h : sigmaCost c = 0) : c = NewcombChoice.oneBox := by
 110  cases c with
 111  | oneBox => rfl
 112  | twoBox => exfalso; simp [sigmaCost] at h
 113
 114/-! ## Master certificate -/
 115
 116/-- **NEWCOMB RESOLUTION MASTER CERTIFICATE.** -/
 117structure NewcombResolutionCert where
 118  one_box_preserves_sigma : sigmaCost NewcombChoice.oneBox = 0
 119  two_box_breaks_sigma : sigmaCost NewcombChoice.twoBox = 1
 120  sigma_ordering :
 121    sigmaCost NewcombChoice.oneBox < sigmaCost NewcombChoice.twoBox
 122  one_box_under_constraint :
 123    ∀ (c : NewcombChoice), sigmaCost c = 0 → c = NewcombChoice.oneBox
 124  perfect_prediction_dominance :
 125    expectedValue NewcombChoice.oneBox 1 - expectedValue NewcombChoice.twoBox 1
 126      = 999000
 127
 128/-- The master certificate is inhabited. -/
 129def newcombResolutionCert : NewcombResolutionCert where
 130  one_box_preserves_sigma := oneBox_preserves_sigma
 131  two_box_breaks_sigma := twoBox_creates_sigma_imbalance
 132  sigma_ordering := sigmaCost_ordering
 133  one_box_under_constraint := oneBox_dominates_under_sigma_conservation
 134  perfect_prediction_dominance := oneBox_dominates_at_perfect_prediction
 135
 136end
 137
 138end NewcombParadox
 139end Decision
 140end IndisputableMonolith
 141