finite_resolution_no_chart
plain-language theorem explainer
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.
Claim. If $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.