DirectedRefinement
plain-language theorem explainer
DirectedRefinement encodes a countable chain of recognizers on a space C in which each subsequent recognizer is finer than the last. Workers on the effective-manifold limit in Recognition Science invoke this structure when they state the U1 hypothesis bundle. The definition is direct; the attached monotone_refines result follows 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 type $C$ consists of a family of event types $E_i$ ($i : ℕ$), recognizers $R_i : Recognizer(C, E_i)$, and a proof that $R_{i+1}$ is finer than $R_i$ for every $i$.
background
The module EffectiveManifold formalizes the structural conditions under which a directed refinement of recognition quotients produces an effective manifold. It addresses four open problems labeled U1–U4 that correspond to the hypotheses of Assumption 2.11 in the paper. U1 is realized by the bundle EffectiveManifoldHypotheses; U2 by the convergence predicate RefinementConverges; U3 by DimensionInvariant; and U4 by NonCollapseCondition. A DirectedRefinement supplies the underlying directed system of recognizers indexed by ℕ together with the refinement ordering IsFinerThan'.
proof idea
The structure itself is a definition and carries no proof. The monotone_refines theorem proceeds by induction on the inequality hij. The base case applies isFinerThan'_refl. The successor case composes the given refines field with isFinerThan'_trans.
why it matters
DirectedRefinement is the central object that feeds EffectiveManifoldHypotheses, RefinementConverges, DimensionInvariant, NonCollapseCondition, and the derived theorems convergence_implies_identity and nonCollapse_monotone_automatic. It supplies the directed chain required for the effective-manifold assumption (Assumption 2.11) and therefore sits at the root of U1–U4. In the broader Recognition Science setting it supplies the countable refinement sequence whose limit is expected to realize the three-dimensional manifold arising from the eight-tick octave and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.