eventCount
plain-language theorem explainer
The definition returns the cardinality of the image of a finite set of configurations under the recognizer map. Analysts of the Sleeping Beauty problem cite it when equating halfer credence to sigma-cost per event. The body is a direct one-line extraction of cardinality from the supplied finiteness witness.
Claim. For a set $U$ of configurations such that the image under the recognizer map is finite, the event count equals the cardinality of that image.
background
Recognition Geometry module RG4 formalizes the axiom that every recognizer admits a neighborhood in which only finitely many labels are distinguished. The neighborhood construction collects all lattice cells sharing a given observed label. Upstream results supply the RS-native gauge with unit tick and voxel, together with the lattice neighborhood definition that makes the image finite by construction.
proof idea
The definition is a one-line wrapper that applies toFinset.card directly to the finiteness hypothesis.
why it matters
It supplies the integer event count required by the Sleeping Beauty resolution certificate and the halfer-equals-sigma-cost theorem. The definition realizes the finite-resolution axiom RG4 inside the geometry layer, ensuring consistency with the eight-tick octave that forces discrete local structure. It closes the path from lattice neighborhoods to decision-theoretic cost calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.