finite_resolution_no_chart
Finite resolution axiom implies no recognition chart exists on an infinite neighborhood whose recognizer image is finite. Recognition geometers cite this to obstruct local Euclidean coordinates under RG4. The proof is a direct application of the hypothesis.
claimIf $U$ is an infinite neighborhood of configuration $c$ in local structure $L$ such that recognizer $r$ maps $U$ to a finite set of events, then no recognition chart of dimension $n$ has domain exactly $U$.
background
RecognitionChart is a structure consisting of a neighborhood domain in the local configuration space together with a coordinate map to $R^n$ that is injective on resolution cells and respects indistinguishability. The finite resolution hypothesis is the axiom that no such chart can exist when the neighborhood is infinite yet its image under the recognizer is finite, justified by a cardinality argument that prevents injection of infinitely many points into a finite image. The module develops charts as local coordinate systems that respect recognition structure, with the physical setting that spacetime dimensions count independent ways recognizers distinguish configurations.
proof idea
The proof is a one-line wrapper that applies the finite resolution hypothesis directly.
why it matters in Recognition Science
This theorem is invoked by the contrapositive chart_exists_implies, which concludes that chart existence forces either finite domain or infinite event image. It implements the obstruction theorem referenced in the Recognition Geometry paper, closing the finite-resolution case within the charts module. In the framework it enforces that local manifold structure requires either infinite resolution or infinite events, aligning with the interpretation that spacetime smoothness arises from recognition.
scope and limits
- Does not prove the finite resolution axiom itself.
- Does not fix a specific numerical value for dimension n.
- Does not address neighborhoods whose recognizer image is infinite.
- Does not construct charts under relaxed cardinality conditions.
formal statement (Lean)
184theorem finite_resolution_no_chart (c : C)
185 (U : Set C) (hU : U ∈ L.N c)
186 (hinf : Set.Infinite U) (hfin : (r.R '' U).Finite)
187 (n : ℕ)
188 (h : finite_resolution_no_chart_hypothesis (L := L) (r := r) c U hU hinf hfin n) :
proof body
Term-mode proof.
189 ¬∃ φ : RecognitionChart L r n, φ.domain = U :=
190 h
191
192/-- Contrapositive: If a chart exists, either configs are finite or events are infinite -/