DirectedRefinement
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.