IndisputableMonolith.RecogGeom.EffectiveManifold
The EffectiveManifold module develops refinement relations on recognizers and the hypotheses needed for effective manifold structures in Recognition Geometry. Researchers formalizing composite measurements or quotient spaces cite it when checking monotonicity or convergence of indistinguishability relations. The module supplies definitions for the finer-than order, directed refinements, convergence, dimension invariance, and non-collapse conditions, together with basic lemmas establishing their properties.
claimLet $R_1,R_2$ be recognizers on a configuration space $C$. Define $R_1$ finer than $R_2$ when $c_1sim_{R_1}c_2$ implies $c_1sim_{R_2}c_2$. The module introduces EffectiveManifoldHypotheses as the conjunction of DirectedRefinement, RefinementConverges, DimensionInvariant and NonCollapseCondition on a sequence of such relations.
background
The module sits inside Recognition Geometry and imports the Recognition Quotient construction $C_R=C/ sim$ together with the composite-recognizer theory of the Composition module. The supplied DOC_COMMENT states the core order: $R_1$ is at least as fine as $R_2$ precisely when every identification made by $R_1$ is also made by $R_2$. Sibling definitions then add DirectedRefinement (a directed system of finer relations), RefinementConverges (convergence of the system), DimensionInvariant (preservation of dimension under the quotient), and NonCollapseCondition (prevention of total collapse).
proof idea
This is a definition module. It declares the refinement order IsFinerThan' and immediately records its reflexive and transitive properties. Further definitions introduce DirectedRefinement, RefinementConverges, EffectiveManifoldHypotheses and the two side conditions DimensionInvariant and NonCollapseCondition. Supporting lemmas establish monotonicity of separation, automatic satisfaction of non-collapse, and the implication that convergence forces the identity relation.
why it matters in Recognition Science
The module supplies the refinement order and convergence machinery presupposed by the Refinement Theorem stated in the Composition module. It therefore supplies the geometric substrate on which effective manifolds are erected inside the Recognition Science framework. The status_summary sibling records the net consistency of these hypotheses with the overall chain.
scope and limits
- Does not prove existence of non-trivial effective manifolds.
- Does not link the refinement order to the phi-ladder or mass formula.
- Does not treat Berry creation threshold or Z_cf values.
- Does not establish convergence for arbitrary (non-directed) sequences.
depends on (2)
declarations in this module (12)
-
def
IsFinerThan' -
theorem
isFinerThan'_refl -
theorem
isFinerThan'_trans -
structure
DirectedRefinement -
structure
RefinementConverges -
structure
DimensionInvariant -
structure
NonCollapseCondition -
theorem
monotone_separation_of_refinement -
structure
EffectiveManifoldHypotheses -
theorem
nonCollapse_monotone_automatic -
theorem
convergence_implies_identity -
def
status_summary