finite_resolution_not_injective
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove global finite resolution over the entire space.
- Does not supply an explicit bound on event count in terms of phi-ladder rungs.
- Does not address injectivity questions outside the finite-resolution hypothesis.
- Does not connect the non-injectivity to mass formulas or Berry thresholds.
formal statement (Lean)
108theorem finite_resolution_not_injective (c : C)
109 (h : HasFiniteLocalResolution L r c)
110 (hinf : ∀ U ∈ L.N c, Set.Infinite U) :
111 ∃ U ∈ L.N c, ¬Function.Injective (r.R ∘ Subtype.val : U → E) := by
proof body
Term-mode proof.
112 obtain ⟨U, hU, hfin⟩ := h
113 exact ⟨U, hU, no_injection_on_infinite_finite L r c U hU (hinf U hU) hfin⟩
114
115/-! ## Resolution Count -/
116
117/-- Count of distinct events in a neighborhood (when finite) -/