eventCountFinite_pos
plain-language theorem explainer
The event count for any nonempty finite set of events drawn from the D-cube edge space is strictly positive. Workers formalizing the finite-resolution axiom RG4 cite this to guarantee that every admissible neighborhood registers at least one distinguishable event. The argument is a direct term reduction to the standard cardinality-positivity fact on finite sets.
Claim. Let $E$ be the edge space of the $D$-cube. If $Ssubseteq E$ is finite and nonempty, then $0<|S|$, where $|S|$ is the cardinality supplied by eventCountFinite.
background
The module formalizes axiom RG4: every configuration admits a neighborhood whose image under any recognizer is finite. This supplies the bridge from recognition to discrete physics at fundamental scales via the eight-tick cycle. The type $E$ is defined as the edges of the $D$-cube with cardinality $Dtimes 2^{D-1}$. eventCountFinite converts a finite set $S$ of such events to its cardinality via the coercion to Finset and card.
proof idea
Term-mode proof. It unfolds the definition of eventCountFinite to expose the underlying Finset cardinality, then applies Finset.card_pos.mpr after converting the nonempty hypothesis through Set.Finite.toFinset_nonempty.
why it matters
The lemma is invoked inside finite_resolution_pos to conclude that every finite-resolution neighborhood carries a positive event count. It therefore closes the local half of RG4 inside the Recognition Science chain. The parent theorem finite_resolution_pos quotes the same positivity to obtain an explicit witness $U$ with $0<eventCountFinite(r.R''U)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.