eventCountFinite_pos
plain-language theorem explainer
Any nonempty finite collection of events has positive event count. Workers on finite local resolution in recognition geometry cite this to guarantee distinguishable configurations in bounded regions. The proof reduces directly to the standard fact that nonempty finite sets have positive cardinality via unfolding the count definition.
Claim. If $S$ is a nonempty finite subset of the event space, then the event count of $S$ is positive.
background
The module establishes axiom RG4 that recognition has finite local resolution: for every configuration and recognizer there is a neighborhood whose image under the recognizer is finite. This explains discreteness at fundamental scales through the eight-tick cycle. The event space consists of the edges of the D-cube, with size $D$ times $2^{D-1}$. The event count for a finite set $S$ is defined as the cardinality of its corresponding finite set. Upstream, the spectral emergence provides the structure of the event space, while the ILG action supplies the broader relativistic context.
proof idea
Unfold the definition of the event count to expose the Finset cardinality. Apply the lemma that a Finset has positive cardinality precisely when it is nonempty, using the conversion from the finite set hypothesis and the nonempty hypothesis.
why it matters
It underpins the theorem that finite resolution neighborhoods have positive event count. This advances the RG4 axiom within the Recognition Science framework, connecting to the eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.