DirectedRefinement
DirectedRefinement packages a countable chain of recognizers on a carrier set C such that each successive recognizer refines the previous one. Researchers constructing effective manifolds from recognition quotients cite this structure to encode the directed system required by the U1 hypothesis bundle. The embedded monotone_refines lemma is proved by induction on the index gap, invoking reflexivity and transitivity of the finer-than relation at each step.
claimA directed refinement system on a set $C$ consists of a family of types $E_i$ indexed by $i$ in the natural numbers, together with recognizers $R_i$ from $C$ to $E_i$ such that $R_{i+1}$ is finer than $R_i$ for every $i$.
background
The EffectiveManifold module formalizes the structural conditions under which a directed refinement of recognition quotients produces an effective manifold, addressing open problems U1 through U4. DirectedRefinement supplies the basic directed system for U1; it is built from the Recognizer type and the IsFinerThan' relation imported from the Quotient and Composition modules. The local setting treats these objects as hypothesis bundles rather than axioms, with the conjunction of U2+U3+U4 shown equivalent to the existence of the U1 bundle.
proof idea
The structure is introduced by direct definition of its three fields. The accompanying monotone_refines theorem proceeds by induction on the inequality $i ≤ j$: the reflexive case applies isFinerThan'_refl and the successor case composes the refines field with isFinerThan'_trans.
why it matters in Recognition Science
DirectedRefinement is the core object fed into EffectiveManifoldHypotheses, convergence_implies_identity, DimensionInvariant, and NonCollapseCondition. It directly implements the directed refinement needed for the effective-manifold assumption (Assumption 2.11) and supports the construction of the smooth limit from the phi-ladder and eight-tick structures. The structure closes the scaffolding gap between the raw recognizer chain and the U2 convergence condition.
scope and limits
- Does not encode the convergence condition (U2).
- Does not enforce non-collapse or monotone separation (U4).
- Does not guarantee dimension invariance under choice of sequence (U3).
- Does not supply explicit manifold charts or atlas data.
formal statement (Lean)
57structure DirectedRefinement (C : Type*) where
58 EventType : ℕ → Type*
59 recognizer : (i : ℕ) → Recognizer C (EventType i)
60 refines : ∀ i : ℕ, IsFinerThan' (recognizer (i + 1)) (recognizer i)
61
62/-- The refinement is monotone: later recognizers are always finer. -/
63theorem DirectedRefinement.monotone_refines (sys : DirectedRefinement C)
64 {i j : ℕ} (hij : i ≤ j) :
65 IsFinerThan' (sys.recognizer j) (sys.recognizer i) := by
proof body
Definition body.
66 induction hij with
67 | refl => exact isFinerThan'_refl _
68 | step _ ih =>
69 exact isFinerThan'_trans _ _ _ (sys.refines _) ih
70
71/-- U2: The convergence condition for a directed refinement system.
72The refinement eventually separates any two distinguishable points:
73for any c₁ ≠ c₂ in C, there exists an index i such that R_i
74distinguishes them. -/