pillar3_finite_resolution_obstruction
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of infinite neighborhoods in concrete models.
- Does not construct the recognizer map from cost or distinction functions.
- Does not address topological continuity or measure properties.
- Does not give quantitative bounds on image size or non-injectivity degree.
- Does not treat compositions of multiple recognizers or the induced quotient.
formal statement (Lean)
82theorem pillar3_finite_resolution_obstruction {C E : Type*}
83 [ConfigSpace C] [EventSpace E]
84 (L : LocalConfigSpace C) (r : Recognizer C E)
85 (c : C) (U : Set C) (hU : U ∈ L.N c)
86 (hinf : Set.Infinite U) (hfin : (r.R '' U).Finite) :
87 ¬Function.Injective (r.R ∘ Subtype.val : U → E) :=
proof body
Term-mode proof.
88 no_injection_on_infinite_finite L r c U hU hinf hfin
89
90/-! ## The Fundamental Theorem -/
91
92/-- **FUNDAMENTAL THEOREM OF RECOGNITION GEOMETRY**
93
94 Two configurations are in the same equivalence class if and only if
95 the recognizer assigns them the same event.
96
97 This is the cornerstone: observable space = C / {same events}. -/