eventCount_pos
plain-language theorem explainer
Event count positivity holds for any neighborhood U of a configuration c whose image under the recognizer map is finite. Workers on discrete emergence from recognition geometries cite this to guarantee that finite-resolution neighborhoods yield strictly positive counts. The term-mode proof unfolds the cardinality definition, verifies nonemptiness via membership, and invokes the standard fact that nonempty finite sets have positive cardinality.
Claim. Let $c$ be a configuration and $U$ a neighborhood of $c$ in the local structure. If the image of $U$ under the recognizer map is finite, then the number of distinct events in $U$ is strictly positive.
background
The FiniteResolution module formalizes axiom RG4: recognition has finite local resolution, so that for any configuration and recognizer there exists a neighborhood whose image under the recognizer map is finite. This supplies the bridge from the 8-tick cycle to discrete physics. The eventCount function returns the cardinality of that finite image set. The upstream SleepingBeauty.eventCount supplies the basic counting primitive for distinct events, while RSNativeUnits.U fixes the native gauge with $c=1$.
proof idea
The term proof first unfolds eventCount to expose the underlying Finset cardinality. It obtains $c$ membership in $U$ from the neighborhood predicate, constructs an explicit witness that the image set is nonempty, converts the finite set to a Finset, and applies Finset.card_pos.mpr.
why it matters
The result anchors the finite-resolution side of Recognition Geometry (RG4) by ensuring event counts cannot vanish inside valid neighborhoods. It supports the module's claim that the 8-tick octave forces finite distinguishability and thereby discrete structure. No downstream theorems are recorded, indicating it functions as a basic positivity lemma inside the finite-resolution development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.