thirderCredence
plain-language theorem explainer
The definition assigns the value one third to the credence for heads when counting awakenings under the J-cost functional. Decision theorists working within Recognition Science cite this constant to resolve the Sleeping Beauty paradox as a mismatch of cost measures. It is introduced as a direct numerical assignment without derivation steps.
Claim. The thirder credence is defined to be $1/3$.
background
In the Sleeping Beauty problem a fair coin is flipped. Heads produces one awakening on Monday; tails produces two awakenings (Monday and Tuesday) separated by memory erasure. The module treats the two standard answers as correct under distinct cost functionals: sigma-cost per coin-flip event (with eventCount equal to 2) versus J-cost per distinct awakening experience (with awakeningCount equal to 3). The upstream eventCount definition from the same module supplies the count of distinct coin-flip events as two, while the parallel definition in FiniteResolution counts events inside a finite neighborhood.
proof idea
The declaration is a one-line definition that directly sets the real number to 1/3. No lemmas are applied and no tactics are used; the constant is chosen so that later theorems can equate it to the reciprocal of the awakening count under J-cost.
why it matters
This definition supplies the numerical value for the thirder position and is referenced by the master certificate SleepingBeautyResolutionCert together with the theorem that equates it to jCostPerExperience. It demonstrates that the apparent paradox dissolves once the cost functional is named, consistent with the J-uniqueness property and the Recognition Composition Law in the broader framework. The construction closes one row of the philosophical-paradoxes section in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.