eventCount_pos
Event count positivity holds for any nonempty finite-resolution neighborhood in a recognition geometry: if U belongs to the neighborhood system around c and the recognizer image of U is finite, then the number of distinct events exceeds zero. Researchers modeling discrete spacetime or finite-resolution observers would invoke this to guarantee that local recognition always registers at least one event. The argument is a direct term-mode proof that unfolds the count, establishes membership and nonemptiness of the image set, and applies the cardin
claimLet $C$ be the configuration space equipped with neighborhood system $L$, let $r$ be a recognizer with recognition map $R$, and let $U$ be a neighborhood of $c$ such that $R(U)$ is finite. Then the number of distinct recognition outcomes in $U$ satisfies $0 < |R(U)|$.
background
The module formalizes axiom RG4: finite local resolution, which states that for every configuration $c$ and recognizer $R$ there exists a neighborhood $U$ around $c$ such that $R(U)$ is finite. This constraint explains the apparent discreteness of the universe at fundamental scales through the 8-tick cycle. The function eventCount tallies the distinct images under $R$ within such a $U$ when the image set is finite.
proof idea
The proof is a term-mode reduction. It unfolds eventCount, invokes the neighborhood membership lemma to obtain $c$ in $U$, constructs the explicit nonempty witness $r.R c$ in the image, and concludes by applying Finset.card_pos to the nonempty finite set obtained from Set.Finite.toFinset_nonempty.
why it matters in Recognition Science
This lemma secures the basic positivity property required by the finite local resolution axiom RG4. It ensures that no bounded recognition neighborhood is empty of events, consistent with the 8-tick octave and the emergence of discrete structures. Although it has no recorded downstream uses, it underpins all counting arguments in finite-resolution geometries and closes a potential gap in the discreteness proofs.
formal statement (Lean)
122theorem eventCount_pos (c : C) (U : Set C) (hU : U ∈ L.N c)
123 (hfin : (r.R '' U).Finite) :
124 0 < eventCount r U hfin := by
proof body
Term-mode proof.
125 unfold eventCount
126 have hc : c ∈ U := L.mem_of_mem_N c U hU
127 have hne : (r.R '' U).Nonempty := ⟨r.R c, ⟨c, hc, rfl⟩⟩
128 exact Finset.card_pos.mpr ((Set.Finite.toFinset_nonempty hfin).mpr hne)
129
130/-! ## Resolution Bound -/
131
132/-- Given a finite set of events, count them -/