monotone_separation_of_refinement
plain-language theorem explainer
Monotone separation of distinguishability holds under directed refinement of recognizers. Researchers constructing effective manifolds from recognition quotients cite it to verify non-singularity without additional assumptions. The argument is a direct one-line transfer of the negation of indistinguishability through the refinement map supplied by the DirectedRefinement structure.
Claim. Let $sys$ be a directed refinement system of recognizers over a type $C$ of configurations. For every natural number $i$ and configurations $c_1, c_2$, if $c_1$ and $c_2$ are distinguishable by the recognizer at stage $i$, then they remain distinguishable by the recognizer at stage $i+1$.
background
The EffectiveManifold module formalizes structural conditions for a directed refinement of recognition quotients to yield an effective manifold, addressing open problems U1–U4 from the paper. A DirectedRefinement structure packages a sequence of recognizers indexed by natural numbers together with IsFinerThan' maps ensuring each later recognizer is strictly finer than the previous. Indistinguishability is the relation negated in the statement; the module treats U1 as a bundled hypothesis structure whose fields encode U2 (RefinementConverges), U3 (DimensionInvariant), and U4 (NonCollapseCondition).
proof idea
The term-mode proof introduces the stage index $i$ and pair $c_1, c_2$, then applies the exact match of the negated indistinguishability hypothesis to the image under the refines map of the DirectedRefinement instance at that stage.
why it matters
The theorem supplies the monotone separation property required for U4 (NonCollapseCondition). It is invoked directly by nonCollapse_monotone_automatic to derive U4 automatically from U2 plus refinement, and is summarized in status_summary as the proved component of the U1 bundle. In the Recognition Science setting this closes the non-singularity requirement for effective-manifold constructions without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.