chart_exists_implies
plain-language theorem explainer
A recognition chart on a local configuration space must have either a finite domain or an infinite image under the recognizer map. Researchers deriving manifold structure from recognition geometry cite this when characterizing local coordinate assignments. The proof is a short contradiction that negates the conclusion, extracts a neighborhood point via the chart's domain property, and applies the no-chart hypothesis directly to reach absurdity.
Claim. Let $L$ be a local configuration space on configurations $C$, $r: C→ E$ a recognizer, and $n∈ℕ$. If $φ$ is a recognition chart for $L,r,n$ with $c$ in its domain, and if no recognition chart exists on any infinite neighborhood $U$ of $c$ whose image under $r$ is finite, then the domain of $φ$ is finite or the image of the domain under $r$ is infinite.
background
The module develops the link between recognition geometry and classical manifold theory. A recognition chart is a local coordinate map on a neighborhood domain that is injective on resolution cells and sends indistinguishable configurations to the same point in $ℝ^n$. The module assumes a local configuration space $L$ whose neighborhoods satisfy RG4 finite-resolution constraints and a recognizer $r$ that produces events $E$ whose finite images block continuous injections to $ℝ^n$ on infinite sets.
proof idea
Proof by contradiction: assume the domain is infinite while its image under $r$ is finite. The tactic obtains the pair of negated conjuncts, extracts a witnessing point $c'$ from the chart's domain_is_nbhd field, then applies the supplied no-chart hypothesis at that point and domain to derive an immediate contradiction with the existence of $φ$.
why it matters
The result supplies the contrapositive half of the chart-existence characterization, directly supporting the atlas_covers_quotient construction and the smooth-structure emergence section. It encodes the finite-resolution obstruction that prevents charts on infinite neighborhoods with finite event images, thereby tightening the bridge from discrete recognition to differential geometry in the Recognition Science setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.