locally_discrete_finite_classes
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish a uniform finite bound independent of the neighborhood.
- Does not prove global finiteness of the entire configuration space.
- Does not relate the finite cardinality to specific phi-ladder rungs or RS-native constants.
- Does not address continuity or injectivity properties beyond the local neighborhood.
formal statement (Lean)
79theorem locally_discrete_finite_classes
80 (h : IsLocallyDiscrete L r) (c : C) :
81 ∃ U ∈ L.N c, (r.R '' U).Finite :=
proof body
Term-mode proof.
82 h c
83
84/-! ## No Continuous Injection Theorem -/
85
86/-- **Key Insight**: If a neighborhood has infinite configurations but finite
87 events, then the recognizer cannot be injective on that neighborhood.
88
89 This explains why discrete recognition geometry fundamentally differs
90 from continuous Euclidean geometry. -/