eventCount
plain-language theorem explainer
eventCount computes the cardinality of the image of a finite set U of configurations under the recognizer map. Decision theorists resolving the Sleeping Beauty problem cite it to set sigma-cost per event to the reciprocal of that count. The definition is realized as a direct extraction of the finite-set cardinality from the supplied finiteness witness.
Claim. Let $U$ be a set of configurations such that the image of $U$ under the recognizer map is finite. The event count is the cardinality of that image.
background
The module formalizes axiom RG4: every configuration admits a neighborhood whose image under the recognizer is finite, supplying the bridge from recognition to discrete physics via the eight-tick cycle. Upstream, RecognitionLatticeFromRecognizer.neighborhood collects all cells sharing an observed label, while RSNativeUnits.U fixes the native gauge with tau0 equal to one tick and ell0 equal to one voxel. The Sleeping Beauty eventCount supplies the model case of two distinct coin-flip events.
proof idea
One-line wrapper that applies the cardinality operation to the finite set supplied by the finiteness hypothesis.
why it matters
The definition is invoked by SleepingBeauty.halfer_eq_per_event and SleepingBeautyResolutionCert to equate halfer credence with sigma-cost per event. It directly implements the finite-resolution constraint of RG4 and the eight-tick octave that forces discreteness at fundamental scales. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.