finite_resolution_event_in_finite
plain-language theorem explainer
If a recognizer satisfies finite local resolution at configuration c, then the event r.R c belongs to some finite set of events. Researchers deriving discreteness of observable states from recognition axioms would cite the result when showing that local neighborhoods yield only finitely many distinguishable outputs. The argument is a direct extraction: the hypothesis supplies a neighborhood U whose image under r.R is finite, and membership of r.R c follows by construction of the image.
Claim. If recognizer $r$ has finite local resolution at configuration $c$ (i.e., there exists neighborhood $U$ of $c$ such that the image set $r.R(U)$ is finite), then there exists a finite set $S$ of events such that $r.R(c) ∈ S$.
background
The module formalizes axiom RG4: recognition has finite local resolution. For every configuration $c$ and recognizer $r$, a neighborhood $U$ exists around $c$ such that only finitely many distinct events appear in $r.R(U)$. This supplies the bridge from recognition geometry to discrete physics, because the 8-tick cycle already bounds distinguishable states inside any local region. HasFiniteLocalResolution is the predicate that encodes the axiom: it asserts existence of $U ∈ L.N c$ with $(r.R '' U).Finite$. The codomain $E$ is the set of edges of the $D$-cube, whose cardinality is $D × 2^{D-1}$.
proof idea
The term proof unpacks the hypothesis $h$ via obtain to extract the witnessing neighborhood $U$ together with the finiteness claim $hfin$. It then forms the finite set as the direct image $r.R '' U$ and verifies that $r.R c$ lies in this image by the membership witness supplied inside $h$. No additional lemmas are invoked beyond the definition of image and the local neighborhood predicate.
why it matters
The declaration feeds the parent definition finite_resolution_status, which collects the finite-resolution properties and states that the 8-tick atomicity bounds the number of distinguishable states in any local region. It realizes the RG4 axiom inside the Recognition Geometry module and thereby supports the claim that finite resolution is a fundamental feature rather than a measurement artifact. The result sits downstream of the LocalConfigSpace and Recognizer structures and upstream of global discreteness arguments that invoke the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.