finite_resolution_not_injective
plain-language theorem explainer
Finite local resolution at c, together with the assumption that every neighborhood of c is infinite, forces the recognizer map to be non-injective on at least one such neighborhood. Researchers deriving discrete geometry from recognition axioms cite this to show that finite distinguishability is incompatible with injective embeddings on infinite sets. The proof is a one-line wrapper that extracts the finite-image neighborhood from HasFiniteLocalResolution and applies the supporting non-injection lemma.
Claim. Let $L$ be a local configuration space on $C$, $r$ a recognizer into event space $E$. If there exists a neighborhood $U$ of $c$ such that the image $r.R(U)$ is finite, and every neighborhood of $c$ is infinite, then there exists a neighborhood $U$ of $c$ on which the restriction of $r.R$ fails to be injective.
background
Module RG4 formalizes axiom that any recognizer has finite local resolution: for each configuration $c$ there is a neighborhood $U$ in the system $L.N c$ such that only finitely many distinct events are observed. HasFiniteLocalResolution $L$ $r$ $c$ is the proposition asserting exactly this existence of a finite-image neighborhood. The module situates the constraint inside the eight-tick cycle that bounds distinguishable states at each point.
proof idea
One-line wrapper. The obtain tactic extracts the witnessing neighborhood $U$ together with its finiteness witness from the hypothesis HasFiniteLocalResolution. The exact tactic then feeds $U$, the infiniteness supplied by the third hypothesis, and the finiteness witness into the sibling lemma no_injection_on_infinite_finite.
why it matters
The corollary is invoked inside the finite_resolution_status definition that records the physical reading of RG4 in terms of bounded ledger updates under eight-tick atomicity. It closes the local step from the Recognition Composition Law and phi-forcing to the requirement that emergent geometries be discrete, consistent with the forced $D=3$ and the alpha band. No scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.