IndisputableMonolith.Decision.SleepingBeauty
The SleepingBeauty module formalizes the Sleeping Beauty paradox inside Recognition Science decision theory by defining halfer credence as 1/2 and thirder credence as 1/3. It introduces eventCount and awakeningCount measures together with sigmaCostPerEvent and jCostPerExperience to test consistency. The module consists of direct definitions plus one-line equality lemmas that verify each credence under its matching cost model.
claimThe module defines halfer credence $1/2$ and thirder credence $1/3$, with event-based cost per coin flip and $J$-cost per awakening, proving consistency of the halfer position under event cost and the thirder position under experience cost.
background
This module belongs to the Decision domain and imports the RS time quantum from Constants together with the cost functions from Cost. The J-cost is the recognition cost $J(x) = (x + x^{-1})/2 - 1$. The Sleeping Beauty setup is modeled via eventCount for the coin toss and awakeningCount for observer experiences, yielding the two standard answers of 1/2 and 1/3.
proof idea
This is a definition module that introduces the two credences and their supporting cost functions; the equalities such as halfer_eq_per_event and thirder_eq_per_experience are one-line wrappers that substitute the counts into the respective cost definitions.
why it matters in Recognition Science
The module supplies the decision-theoretic treatment of Sleeping Beauty inside the Recognition Science framework, showing how each standard answer aligns with a distinct cost measure. It connects the halfer position to event-based costs and the thirder position to experience-based J-costs, providing concrete instances of cost-based decision evaluation.
scope and limits
- Does not resolve which credence is correct in absolute terms.
- Does not incorporate quantum mechanics or other physical dynamics.
- Does not extend the analysis to variants with different awakening schedules.
- Does not reference the forcing chain T0-T8 or the phi-ladder.
depends on (2)
declarations in this module (15)
-
inductive
SleepingBeautyAnswer -
def
name -
def
eventCount -
def
awakeningCount -
def
halferCredence -
def
thirderCredence -
theorem
halfer_eq_per_event -
theorem
thirder_eq_per_experience -
def
sigmaCostPerEvent -
def
jCostPerExperience -
theorem
halfer_correct_under_event_cost -
theorem
thirder_correct_under_experience_cost -
theorem
paradox_is_category_error -
structure
SleepingBeautyResolutionCert -
def
sleepingBeautyResolutionCert