monotone_separation_of_refinement
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that any refinement sequence converges to a smooth limit manifold.
- Does not establish dimension invariance across different refinement paths.
- Does not address mass formulas, phi-ladder rungs, or Berry creation thresholds.
- Does not discharge the full EffectiveManifoldHypotheses bundle on its own.
Lean usage
theorem nonCollapse_monotone_automatic (sys : DirectedRefinement C) : ∀ i c₁ c₂, ¬Indistinguishable (sys.recognizer i) c₁ c₂ → ¬Indistinguishable (sys.recognizer (i + 1)) c₁ c₂ := monotone_separation_of_refinement sysformal statement (Lean)
108theorem monotone_separation_of_refinement (sys : DirectedRefinement C) :
109 ∀ i : ℕ, ∀ c₁ c₂ : C,
110 ¬Indistinguishable (sys.recognizer i) c₁ c₂ →
111 ¬Indistinguishable (sys.recognizer (i + 1)) c₁ c₂ := by
proof body
Term-mode proof.
112 intro i c₁ c₂ hne habs
113 exact hne (sys.refines i c₁ c₂ habs)
114
115/-! ## U1: The Effective Manifold Bundle -/
116
117/-- U1: The complete hypothesis bundle for the effective-manifold assumption.
118This packages U2 + U4 (U3 is a consequence when the limit exists). -/