thirder_correct_under_experience_cost
plain-language theorem explainer
The result equates the thirder credence of one-third with the J-cost per experience in the Sleeping Beauty setup. Decision theorists and philosophers working on the paradox under Recognition Science cost functionals would cite this equality to separate the two positions. The proof is a one-line term that unfolds the three definitions and normalizes the arithmetic.
Claim. The thirder credence equals the J-cost per experience, where the thirder credence is $1/3$ and the J-cost per experience is one divided by the number of distinct awakening experiences.
background
The module treats the Sleeping Beauty paradox as a choice between cost functionals rather than a single probability question. Awakening count is defined as the number of distinct possible awakening experiences and equals 3. J-cost per experience is then one divided by that count, while the thirder credence is defined directly as one-third. Upstream, the cost of a recognition event is its J-cost from the ObserverForcing module, and the multiplicative recognizer supplies a derived cost on positive ratios.
proof idea
The proof is a one-line term that unfolds thirderCredence, jCostPerExperience, and awakeningCount, then applies norm_num to reduce the resulting numerical expression to an identity.
why it matters
This theorem supplies the thirder half of the master certificate sleepingBeautyResolutionCert, which records that both positions are correct under their own cost and that the paradox is therefore a category error. It draws on the J-cost definition from ObserverForcing and aligns with J-uniqueness in the forcing chain. The result closes the philosophical-paradox row in the framework by exhibiting explicit cost functionals for each answer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.