HasFiniteResolution
plain-language theorem explainer
A recognizer has finite resolution on a local configuration space precisely when every configuration admits only finitely many distinguishable events. Researchers modeling discrete spacetime or recognition-based emergence cite this as the global form of axiom RG4. The definition is the universal closure of the local finite-resolution predicate.
Claim. A recognizer $r$ has finite resolution on local configuration space $L$ if for every configuration $c$ the recognizer distinguishes only finitely many events in some neighborhood of $c$.
background
Recognition geometry requires that any recognizer distinguishes only finitely many configurations inside bounded neighborhoods; this is axiom RG4. The supporting local predicate asserts that a single configuration $c$ maps under the recognizer to a finite event set. Upstream results supply the edge-counting function $E$ for $D$-cubes and spectral-emergence bounds that limit distinguishable states via phi-ladder rungs.
proof idea
The declaration is a direct definition equating the global property to the universal quantification of the local finite-resolution predicate at every configuration. No lemmas or tactics are invoked beyond the quantifier.
why it matters
This supplies the global statement of RG4 that defines local discreteness and assembles the full RecognitionGeometry structure. It is instantiated by the master theorem showing that the eight-tick finite-resolution hypothesis yields the property. In the framework it realizes the finite resolution enforced by the eight-tick octave, which forces the discrete character of emergent geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.