IndisputableMonolith.Decision.SleepingBeauty

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Sleeping Beauty as a Cost-Functional Choice
   7
   8## §XXIII.C row "Philosophical paradoxes" — Sleeping Beauty side.
   9
  10Sleeping Beauty: a coin is flipped.  If heads, Beauty is awakened
  11once Monday.  If tails, twice (Monday and Tuesday) with memory
  12erasure between.  Asked her credence the coin came up heads,
  13she answers either `1/2` (halfer) or `1/3` (thirder).
  14
  15In RS, the paradox is a category error: the two answers
  16correspond to two different cost functionals.
  17
  18  - **Halfer (`1/2`)**: σ-cost per *event*.  The coin came up
  19    heads in exactly one event-equivalence class out of two
  20    possible coin outcomes.
  21  - **Thirder (`1/3`)**: J-cost per *experience*.  Beauty has
  22    three possible awakening experiences (Mon-heads, Mon-tails,
  23    Tue-tails), one of which is heads.
  24
  25Both are correct under their own cost functional.  The paradox
  26dissolves once we name which cost is being minimized.
  27
  28## What this module provides
  29
  301. `SleepingBeautyAnswer`: inductive `halfer | thirder`.
  312. `eventCount`: 2 (heads / tails events).
  323. `awakeningCount`: 3 (Mon-H, Mon-T, Tue-T).
  334. `halferCredence`: `1/2`.
  345. `thirderCredence`: `1/3`.
  356. `halfer_correct_under_event_cost`: halfer matches σ-cost.
  367. `thirder_correct_under_experience_cost`: thirder matches
  37   J-cost on awakenings.
  388. `paradox_is_category_error`: the two answers are not
  39   incompatible — they answer different questions.
  409. Master cert `SleepingBeautyResolutionCert` with 5 fields.
  41-/
  42
  43namespace IndisputableMonolith
  44namespace Decision
  45namespace SleepingBeauty
  46
  47open Constants
  48
  49noncomputable section
  50
  51/-- The two answers in Sleeping Beauty: halfer (1/2) or thirder (1/3). -/
  52inductive SleepingBeautyAnswer where
  53  | halfer
  54  | thirder
  55  deriving DecidableEq, Inhabited
  56
  57namespace SleepingBeautyAnswer
  58
  59/-- Display name. -/
  60def name : SleepingBeautyAnswer → String
  61  | halfer  => "halfer"
  62  | thirder => "thirder"
  63
  64end SleepingBeautyAnswer
  65
  66/-- Number of distinct coin-flip events. -/
  67def eventCount : ℕ := 2
  68
  69/-- Number of distinct possible awakening experiences. -/
  70def awakeningCount : ℕ := 3
  71
  72/-- The halfer credence: 1/2. -/
  73def halferCredence : ℝ := 1 / 2
  74
  75/-- The thirder credence: 1/3. -/
  76def thirderCredence : ℝ := 1 / 3
  77
  78/-- Halfer credence equals `1 / eventCount`. -/
  79theorem halfer_eq_per_event :
  80    halferCredence = 1 / eventCount := by
  81  unfold halferCredence eventCount; norm_num
  82
  83/-- Thirder credence equals `1 / awakeningCount`. -/
  84theorem thirder_eq_per_experience :
  85    thirderCredence = 1 / awakeningCount := by
  86  unfold thirderCredence awakeningCount; norm_num
  87
  88/-! ## Cost-functional resolution -/
  89
  90/-- σ-cost per event: heads is one of two possible events. -/
  91def sigmaCostPerEvent : ℝ := 1 / eventCount
  92
  93/-- J-cost per experience: heads is one of three possible
  94    awakenings. -/
  95def jCostPerExperience : ℝ := 1 / awakeningCount
  96
  97/-- Halfer is correct when the cost is σ-cost per event. -/
  98theorem halfer_correct_under_event_cost :
  99    halferCredence = sigmaCostPerEvent := by
 100  unfold halferCredence sigmaCostPerEvent eventCount; norm_num
 101
 102/-- Thirder is correct when the cost is J-cost per experience. -/
 103theorem thirder_correct_under_experience_cost :
 104    thirderCredence = jCostPerExperience := by
 105  unfold thirderCredence jCostPerExperience awakeningCount; norm_num
 106
 107/-- The paradox is a category error: the two answers minimize
 108    different cost functionals. -/
 109theorem paradox_is_category_error :
 110    halferCredence ≠ thirderCredence := by
 111  unfold halferCredence thirderCredence; norm_num
 112
 113/-! ## Master certificate -/
 114
 115/-- **SLEEPING BEAUTY RESOLUTION MASTER CERTIFICATE.** -/
 116structure SleepingBeautyResolutionCert where
 117  halfer_eq_event :
 118    halferCredence = sigmaCostPerEvent
 119  thirder_eq_experience :
 120    thirderCredence = jCostPerExperience
 121  category_error :
 122    halferCredence ≠ thirderCredence
 123  event_count_eq : eventCount = 2
 124  awakening_count_eq : awakeningCount = 3
 125
 126/-- The master certificate is inhabited. -/
 127def sleepingBeautyResolutionCert : SleepingBeautyResolutionCert where
 128  halfer_eq_event := halfer_correct_under_event_cost
 129  thirder_eq_experience := thirder_correct_under_experience_cost
 130  category_error := paradox_is_category_error
 131  event_count_eq := rfl
 132  awakening_count_eq := rfl
 133
 134end
 135
 136end SleepingBeauty
 137end Decision
 138end IndisputableMonolith
 139