eventCount
plain-language theorem explainer
eventCount returns the cardinality of the image of a set U of configurations under the recognizer map r.R whenever that image is finite. Researchers formalizing finite local resolution in Recognition Geometry cite it when bounding distinguishable states inside a neighborhood. The definition is a direct one-line extraction of the cardinality from the supplied finiteness witness.
Claim. Let $U$ be a subset of configurations such that the image under the recognizer map is finite. Then the event count of $U$ equals the cardinality of that image.
background
The RecogGeom.FiniteResolution module states axiom RG4: every configuration admits a neighborhood whose image under any recognizer is finite. This supplies the bridge from recognition to discrete physics via the eight-tick cycle. The neighborhood construction appears upstream in RecognitionLatticeFromRecognizer as the set of all cells sharing a fixed observed label. RSNativeUnits.U fixes the native gauge with one tick and one voxel as units.
proof idea
One-line wrapper that applies toFinset.card to the finiteness hypothesis.
why it matters
The definition implements the counting step required by RG4 finite local resolution. It is invoked by SleepingBeauty.halfer_eq_per_event and sigmaCostPerEvent to set halfer credence equal to one over the event count, and by SleepingBeautyResolutionCert to certify the halfer-thirder distinction. It therefore supplies the concrete cardinality that lets the eight-tick octave enforce finite resolution in decision models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.