eventCount_pos
plain-language theorem explainer
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
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.