eventCountFinite
plain-language theorem explainer
eventCountFinite maps each finite set of events to its cardinality in natural numbers. Researchers modeling discrete geometries under Recognition Science would cite it when establishing positive counts inside finite-resolution neighborhoods. The definition is a one-line wrapper that converts the finiteness hypothesis to a Finset and extracts its card.
Claim. For a finite set $Ssubseteq E$, the event count is defined to be the cardinality $|S|$, where $E$ is the event space of the recognition geometry.
background
The Recognition Geometry module formalizes axiom RG4: recognition has finite local resolution. For every configuration $c$ and recognizer $R$ there exists a neighborhood $U$ around $c$ such that $R(U)$ is finite. This supplies the bridge from recognition to discrete physics at fundamental scales, with the 8-tick cycle providing the concrete finite resolution mechanism. The type $E$ is imported from SpectralEmergence, where it denotes the edges of the $D$-cube with $|E|=Dcdot2^{D-1}$. Upstream results supply collision-free and algebraic-tautology properties that keep the event sets well-behaved.
proof idea
The definition is implemented directly as hfin.toFinset.card. It is a one-line wrapper that applies the standard Mathlib cardinality operation on finite sets.
why it matters
This definition is invoked by eventCountFinite_pos and finite_resolution_pos, which prove that finite-resolution neighborhoods contain a positive number of events. It therefore realizes the counting step required by RG4 inside the Recognition Science framework, linking the eight-tick octave to the emergence of $D=3$ spatial dimensions and the phi-ladder mass formula. It closes one link in the chain from self-similar fixed points to observable discreteness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.