convergence_implies_identity
plain-language theorem explainer
A directed refinement system on space C that satisfies the convergence condition forces the intersection of all induced equivalence relations to be the diagonal: any two points indistinguishable by every recognizer must coincide. Researchers formalizing the effective manifold limit under Recognition Science Assumption 2.11 cite this to confirm point separation in the limit. The proof is a one-line wrapper extracting the eventually_separates field from the RefinementConverges hypothesis.
Claim. Let $(R_i)_{i∈ℕ}$ be a directed refinement system on a space $C$. If the system converges, then for all $c_1,c_2∈C$, if $c_1$ and $c_2$ remain indistinguishable under every $R_i$, then $c_1=c_2$.
background
The EffectiveManifold module formalizes structural conditions U1–U4 under which a directed refinement of recognition quotients yields an effective manifold. A DirectedRefinement consists of a sequence of recognizers indexed by ℕ that are monotonically finer under the IsFinerThan' relation. RefinementConverges is the U2 hypothesis bundle whose eventually_separates field encodes the density condition that the refinement separates all distinct points in the base space C. The module addresses open problems tied to the paper's Assumption 2.11, which requires a directed refinement, a smooth D-manifold limit, and converging coarse-graining maps; the present theorem isolates the separation property internal to that assumption.
proof idea
The proof is a one-line wrapper that applies the eventually_separates field of the supplied RefinementConverges hypothesis directly to the given system.
why it matters
This theorem supplies the core separation property for U2 inside the EffectiveManifoldHypotheses bundle and is invoked by the status_summary definition that reports formalization status for the open problems. It directly supports the paper's Assumption 2.11 by confirming that convergence implies the intersection of equivalence relations is the diagonal, a prerequisite for the effective manifold construction. The result sits within the Recognition Science framework's treatment of directed refinements leading to the D=3 manifold limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.