IsLocallyDiscrete
plain-language theorem explainer
A local configuration space L paired with recognizer r is locally discrete precisely when r maps every neighborhood to a finite set of distinguishable states. Physicists constructing discrete spacetime from recognition axioms cite this to enforce finite local distinguishability as a primitive constraint. The definition is a direct one-line alias to the HasFiniteResolution predicate.
Claim. A local configuration space $L$ together with recognizer $r$ is locally discrete when, for every configuration $c$, there exists a neighborhood $U$ of $c$ such that the image of $U$ under $r$ is finite.
background
The Recognition Geometry module formalizes axiom RG4: finite local resolution. HasFiniteResolution requires that for every configuration the recognizer distinguishes only finitely many states inside some neighborhood. The neighborhood predicate, imported from RecognitionLatticeFromRecognizer, collects all lattice cells sharing a given observed label. This setting assumes the eight-tick cycle supplies the atomic bound that makes local resolution finite.
proof idea
The definition is a one-line alias that directly invokes HasFiniteResolution, inheriting its universal quantification over all configurations.
why it matters
IsLocallyDiscrete supplies the hypothesis for locally_discrete_finite_classes, which concludes that every neighborhood image is finite, and for physical_interpretation_finite_resolution, which ties the property to the eight-tick atomicity of Recognition Science. It encodes the RG4 axiom that any recognition geometry must obey finite distinguishability, bridging abstract recognition to discrete physical scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.