eventCount
plain-language theorem explainer
eventCount fixes the number of distinct coin-flip outcomes at two for the Sleeping Beauty setup. Decision theorists working inside Recognition Science cite it when separating sigma-cost per event from J-cost per experience. The definition is a direct constant assignment of the natural number 2.
Claim. The number of distinct coin-flip events is defined as the constant 2.
background
The Sleeping Beauty module frames the classic paradox as a category error between two cost functionals. Halfer credence uses sigma-cost per event while thirder credence uses J-cost per experience. eventCount supplies the event denominator for the halfer side, set to heads versus tails.
proof idea
One-line definition that assigns the constant 2.
why it matters
This definition supplies the denominator for halferCredence = 1/eventCount and for sigmaCostPerEvent. It feeds directly into halfer_correct_under_event_cost and the master certificate SleepingBeautyResolutionCert. The placement anchors the event-based accounting that dissolves the paradox once the cost functional is named, consistent with J-cost convexity from PhiForcingDerived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.