pillar3_finite_resolution_obstruction
plain-language theorem explainer
If a neighborhood U around a configuration c contains infinitely many points but the recognizer maps U to only finitely many events, the restricted map from U to events cannot be injective. Researchers formalizing discrete spacetime or recognition-based physics would cite this to show finite resolution is unavoidable. The proof is a one-line term application of the general non-injectivity fact for infinite-to-finite images under the recognizer composition.
Claim. Let $C$ be a configuration space and $E$ an event space. Let $L$ be a local configuration space on $C$ and $r$ a recognizer. For $c$ in $C$ and $U$ a neighborhood of $c$ in $L$ (i.e., $U$ belongs to the neighborhood family of $L$ at $c$), if $U$ is infinite but the image of $U$ under the recognition map of $r$ is finite, then the recognition map restricted to $U$ is not injective.
background
Recognition Geometry equips configuration spaces with local neighborhoods and recognizers that induce event assignments. From upstream, a ConfigSpace consists of an empty configuration, a commutative monoid join, a consistency predicate, and an independence relation. LocalConfigSpace supplies the neighborhood family $N(c)$ for each configuration, while a Recognizer supplies the map $R$ from configurations to events in $E$ together with the EventSpace structure on $E$.
proof idea
The proof is a term-mode one-line wrapper. It applies the general non-injectivity result for maps from an infinite set to a finite image, instantiated at the recognizer map composed with the subtype inclusion of the neighborhood $U$. No additional tactics or reductions are used.
why it matters
This result supplies Pillar 3 (finite resolution is fundamental) in the Foundations module and is invoked by the foundations_status definition that summarizes the three pillars and the Fundamental Theorem. The Fundamental Theorem asserts that configurations are equivalent precisely when the recognizer assigns them the same event. It aligns with the framework's discrete structure, including the eight-tick octave and $D=3$ dimensions, and closes the argument that finite events force coarse-graining without leaving scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.