SleepingBeautyResolutionCert
plain-language theorem explainer
The Sleeping Beauty resolution certificate is a structure recording that the halfer credence equals sigma-cost per event, the thirder credence equals J-cost per experience, the two credences differ, and the counts are fixed at two events and three awakenings. Decision theorists applying Recognition Science to paradoxes would cite it to treat the problem as a category error between distinct cost functionals. The structure is defined directly from the module's prior count constants and cost-matching lemmas.
Claim. A certificate consisting of the assertions that halfer credence equals sigma-cost per event, thirder credence equals J-cost per experience, halfer credence differs from thirder credence, event count equals 2, and awakening count equals 3.
background
In the Recognition Science treatment of Sleeping Beauty, a coin flip yields either one awakening (heads) or two (tails) with memory erasure. The module distinguishes sigma-cost per event from J-cost per experience. Event count is defined as 2 and awakening count as 3. Halfer credence is 1/2 and thirder credence is 1/3. Sigma-cost per event is 1 over event count while J-cost per experience is 1 over awakening count. Upstream lemmas establish that the halfer position matches sigma-cost and the thirder position matches J-cost.
proof idea
The declaration is a structure definition that packages five fields. No tactics are required. The downstream inhabitant sleepingBeautyResolutionCert populates the fields by applying the lemmas halfer_correct_under_event_cost, thirder_correct_under_experience_cost, and paradox_is_category_error together with reflexivity on the two count definitions.
why it matters
This certificate supplies the inhabited record that closes the Sleeping Beauty module and witnesses the resolution of the paradox as a category error. It is used by the definition sleepingBeautyResolutionCert to assert that the master certificate is inhabited. In the framework it shows how explicit choice of cost functional (sigma per event versus J per experience) dissolves the apparent contradiction, consistent with the cost distinctions developed in the Cost module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.