locally_discrete_finite_classes
plain-language theorem explainer
In a locally discrete recognition geometry, every neighborhood of a configuration contains only finitely many distinguishable events under the recognizer. Researchers deriving discrete spacetime models or finite-resolution constraints in Recognition Science cite this to ground local discreteness. The proof is a direct one-line term application of the IsLocallyDiscrete hypothesis to the given configuration.
Claim. Let $L$ be a local configuration space and $r$ a recognizer. If $L$ is locally discrete with respect to $r$, then for every configuration $c$ there exists a neighborhood $U$ of $c$ such that the image $r.R(U)$ is a finite set.
background
The module formalizes axiom RG4 of finite local resolution: for every configuration $c$ and recognizer $R$, a neighborhood $U$ exists with $R(U)$ finite. This constraint arises because the eight-tick cycle supplies finite resolution, bridging recognition geometry to observed discreteness at fundamental scales. IsLocallyDiscrete is defined as HasFiniteResolution $L$ $r$, which directly encodes that every neighborhood contains only finitely many distinguishable configurations. The neighborhood operation itself comes from RecognitionLatticeFromRecognizer, selecting all cells sharing an observed label.
proof idea
The proof is a one-line term wrapper that applies the hypothesis $h$ (encoding HasFiniteResolution) directly to the configuration $c$. No additional tactics or lemmas are invoked; the result follows immediately from the definition of local discreteness.
why it matters
This theorem supplies the concrete statement of RG4 inside the Recognition framework, enabling later results on non-injectivity such as finite_resolution_not_injective. It instantiates the general finite-resolution constraint that follows from the eight-tick octave and distinguishes recognition geometry from continuous Euclidean models. No open scaffolding remains; the result is fully proved and ready for use in downstream discreteness arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.