IndisputableMonolith.RecogGeom.EffectiveManifold
The EffectiveManifold module formalizes refinement relations among recognizers to define effective manifold structures in recognition geometry. It introduces IsFinerThan' together with DirectedRefinement, RefinementConverges, DimensionInvariant and NonCollapseCondition, plus supporting lemmas on monotonicity and convergence. The module rests on the quotient and composition constructions and supplies the hypotheses needed for manifold-like behavior without collapse.
claimLet $R_1,R_2$ be recognizers on configuration space $C$. Write $R_1\preceq R_2$ when $c_1\sim_{R_1}c_2$ implies $c_1\sim_{R_2}c_2$. The module defines DirectedRefinement, RefinementConverges, DimensionInvariant and NonCollapseCondition, together with the hypothesis package EffectiveManifoldHypotheses.
background
Recognition Geometry begins with the quotient construction $C_R=C/\sim_R$ (Quotient module) that collapses configurations indistinguishable by a recognizer. The Composition module extends this to composite recognizers and states the Refinement Theorem. EffectiveManifold supplies the refinement order and the auxiliary conditions (monotonic separation, automatic non-collapse, convergence to identity) required to obtain manifold-like quotients that preserve dimension.
proof idea
This is a definition module. It declares the refinement preorder IsFinerThan' and records its reflexivity and transitivity as one-line lemmas. The remaining declarations (monotone_separation_of_refinement, nonCollapse_monotone_automatic, convergence_implies_identity, status_summary) are direct consequences of the definitions; no substantial tactic scripts appear.
why it matters in Recognition Science
The module supplies the refinement infrastructure that the Refinement Theorem (Composition module) requires in order to produce effective manifolds. It encodes the non-collapse and dimension-invariance conditions that keep the quotient compatible with the eight-tick octave and $D=3$ of the forcing chain. No downstream declarations are listed yet.
scope and limits
- Does not construct explicit charts or atlases on the quotient.
- Does not derive the numerical values of constants such as $\alpha^{-1}$.
- Does not address the phi-ladder mass formula or Berry threshold.
- Does not prove existence of effective manifolds, only the required hypotheses.
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