finite_resolution_pos
plain-language theorem explainer
Finite resolution neighborhoods in recognition geometry contain at least one distinguishable event. Researchers modeling discrete spacetime at Planck scales would cite this to guarantee positive event counts inside local neighborhoods. The proof extracts the witnessing neighborhood and finiteness witness directly from the hypothesis then invokes the positivity lemma for finite event sets.
Claim. Let $L$ be a local configuration space over $C$ and $r$ a recognizer. If configuration $c$ satisfies finite local resolution under $L$ and $r$, then there exists a neighborhood $U$ in the neighborhood system of $c$ such that the image of $U$ under $r.R$ is finite and the event count of this finite image is strictly positive.
background
The Recognition Geometry module RG4 formalizes the axiom that recognition admits only finite local resolution: for every configuration $c$ and recognizer $r$ there exists a neighborhood $U$ around $c$ such that $r.R(U)$ is finite. HasFiniteLocalResolution $L$ $r$ $c$ is the predicate asserting exactly this existence of $U$ in $L.N(c)$ with the image finite. The module sits inside the broader Recognition Science setting where the 8-tick cycle supplies the atomicity that makes such finiteness fundamental rather than approximate.
proof idea
The proof is a one-line term wrapper. It obtains the neighborhood $U$ and finiteness witness $hfin$ from the hypothesis, then applies the lemma eventCountFinite_pos to the pair consisting of the recognizer image at $c$ together with the membership proof that $c$ lies in $U$.
why it matters
This result secures the positivity half of the finite-resolution axiom RG4, ensuring that every local neighborhood contains at least one distinguishable event. It directly supports the physical reading that finite resolution arises from the 8-tick octave rather than from measurement limits. No downstream theorems are recorded yet, so the lemma remains a foundational closure for the discreteness claim in the Recognition Geometry layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.