finite_resolution_not_injective
plain-language theorem explainer
Finite local resolution at c, under the assumption that every neighborhood of c is infinite, forces the recognizer map to fail injectivity on at least one such neighborhood. Recognition geometers cite the result when showing that RG4 implies collapse of distinctions inside infinite sets. The proof is a one-line wrapper that extracts the finite-image neighborhood from the resolution hypothesis and invokes the sibling non-injectivity lemma.
Claim. Let $L$ be a local configuration space, $r$ a recognizer from configurations $C$ to events $E$, and $c$ a configuration. If there exists a neighborhood $U$ of $c$ on which the image under $r$ is finite, and if every neighborhood of $c$ is infinite, then there exists a neighborhood $U$ of $c$ such that the map $r$ restricted to $U$ is not injective.
background
Module RG4 encodes axiom that recognition has finite local resolution: for every configuration $c$ and recognizer $r$ there is a neighborhood $U$ around $c$ such that only finitely many distinct events are observed. HasFiniteLocalResolution $L$ $r$ $c$ asserts precisely that such a finite-image neighborhood exists inside the collection $L.N(c)$ of neighborhoods of $c$ supplied by the local configuration space.
proof idea
One-line wrapper that obtains the finite neighborhood witness from the HasFiniteLocalResolution hypothesis and passes it, together with the infinitude assumption on that same neighborhood, directly to the sibling lemma no_injection_on_infinite_finite.
why it matters
The corollary feeds the finite_resolution_status definition, which records that finite resolution corresponds to the 8-tick atomicity bounding the number of distinguishable states. It completes the RG4 step inside Recognition Geometry by converting the finite-image condition into non-injectivity, a prerequisite for discrete emergent geometry. The parent status string lists this result among the verified consequences of the axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.