HasFiniteLocalResolution
plain-language theorem explainer
HasFiniteLocalResolution encodes the local form of axiom RG4: a recognizer maps some neighborhood of configuration c to only finitely many distinct events. Discrete-geometry modelers cite it when deriving bounded resolution from recognition axioms and the eight-tick cycle. The declaration is realized as a direct existential statement over neighborhoods whose image under the event map is finite.
Claim. A recognizer $r$ has finite local resolution at configuration $c$ relative to local configuration space $L$ if there exists a neighborhood $U$ of $c$ such that the image of $U$ under the recognizer's event map is a finite set.
background
Module RecogGeom.FiniteResolution formalizes axiom RG4. LocalConfigSpace equips each configuration with a neighborhood system N. Recognizer supplies the map R from configurations to events E. The definition therefore requires that R(U) remains finite for some U in N(c). Upstream results supply the discrete scales: RS-native units fix the tick and voxel, spectral emergence E counts the edges of the D-cube, and the actualization operator A selects realized configurations. These together ensure that local recognition cannot produce infinitely many distinguishable outcomes.
proof idea
The declaration is a definition whose body is the direct existential quantifier: there exists U belonging to L.N c such that the image set (r.R '' U) is finite. No lemmas are applied and no tactics are used beyond the set-theoretic predicate Finite.
why it matters
HasFiniteLocalResolution supplies the local statement of RG4 and is used by HasFiniteResolution to obtain the global property. Downstream results such as finite_resolution_event_in_finite and finite_resolution_not_injective derive finite event counts and non-injectivity on infinite neighborhoods. It anchors the eight-tick octave by bounding the number of ledger updates observable in any local region, thereby explaining the emergence of discrete geometry from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.