RefinementConverges
plain-language theorem explainer
RefinementConverges encodes the U2 convergence condition requiring that any directed refinement system of recognizers on a set C eventually separates every pair of distinct points. Researchers formalizing the smooth limit of recognition quotients cite this when assembling the structural hypotheses for an effective manifold. The declaration is a pure structural definition that introduces a single field capturing the separation property with no proof obligations.
Claim. Let $sys$ be a directed refinement system on a set $C$. Then $sys$ converges if for all $c_1, c_2 : C$ with $c_1 ≠ c_2$ there exists a stage $i$ such that the recognizer at stage $i$ distinguishes $c_1$ from $c_2$. Equivalently, if two points remain indistinguishable under every recognizer in the system then they are identical.
background
The Effective Manifold Theory module formalizes 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 ℕ together with the monotone refinement relation that each later recognizer is finer than the earlier ones. The convergence condition supplies the U2 density requirement needed for the smooth limit to exist.
proof idea
This is a pure structural definition with no proof body. It directly introduces the Prop-valued structure whose single field eventually_separates encodes the required separation property. No lemmas or tactics are invoked; the definition serves as a hypothesis interface for downstream results.
why it matters
RefinementConverges supplies the U2 component inside the EffectiveManifoldHypotheses bundle that packages the paper's Assumption 2.11. It is invoked by convergence_implies_identity to recover the identity relation and by DimensionInvariant to establish that dimension is independent of refinement choice. The declaration therefore closes one of the four open problems listed in the module documentation and supports the passage from discrete recognition systems to a continuum limit consistent with the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.