sigmaCostPerEvent
plain-language theorem explainer
Defines the σ-cost per event as the reciprocal of the number of coin-flip events. Decision theorists resolving the Sleeping Beauty paradox via cost functionals cite it to equate the halfer credence with event-based costing. The definition is a direct abbreviation that pulls the fixed eventCount value of 2.
Claim. The σ-cost per event is defined by $1/N_e$ where $N_e=2$ is the number of distinct coin-flip events.
background
The module reframes the Sleeping Beauty paradox as a choice between cost functionals rather than incompatible credences. Halfer credence 1/2 matches σ-cost per event while thirder credence 1/3 matches J-cost per experience. eventCount supplies the denominator and is fixed at 2 for the two possible coin outcomes.
proof idea
One-line definition that computes the reciprocal of eventCount in the reals.
why it matters
Supplies the numerical value required by halfer_correct_under_event_cost and the halfer_eq_event field of SleepingBeautyResolutionCert. It instantiates the event-based cost functional that dissolves the paradox as a category error between two distinct minimization targets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.