nonCollapse_monotone_automatic
plain-language theorem explainer
In a directed refinement system of recognizers, distinguishability between configurations at stage i is preserved at stage i+1. Researchers constructing effective manifolds from recognition quotients cite this to confirm that the non-collapse requirement holds without extra assumptions once refinement is given. The proof is a direct one-line application of the monotone separation lemma to the input system.
Claim. Let $sys$ be a directed refinement of recognizers. Then for all stages $i$ and configurations $c_1, c_2$, if $c_1$ and $c_2$ are distinguishable under the recognizer at stage $i$, they remain distinguishable under the recognizer at stage $i+1$.
background
The module formalizes structural conditions U1-U4 under which a directed refinement of recognition quotients yields an effective manifold. A DirectedRefinement is a structure indexed by natural numbers whose recognizer field supplies a sequence of recognizers such that each later one is finer than the earlier, via the IsFinerThan' relation; the structure also carries the monotone_refines theorem establishing that refinement is preserved under index increase. The local setting addresses four open problems: EffectiveManifoldData for the structural bundle (paper Assumption 2.11), RefinementConverges for the density condition (U2), DimensionInvariant for dimension independence (U3), and NonCollapseCondition for non-singularity (U4). The theorem shows that the conjunction of U2 with the refinement property automatically yields the monotone separation component of U4.
proof idea
The proof is a one-line wrapper that applies monotone_separation_of_refinement to the supplied DirectedRefinement system.
why it matters
This declaration shows that the monotone separation property demanded by NonCollapseCondition (U4) follows automatically from the directed refinement structure together with the convergence condition (U2). It therefore contributes to the module theorem establishing equivalence between the conjunction of U2+U3+U4 and the existence of the U1 bundle. In the Recognition Science framework the result closes a structural requirement in the passage from recognition quotients to effective manifolds without adding independent hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.