DimensionInvariant
plain-language theorem explainer
DimensionInvariant encodes that any two convergent directed refinement systems on the same base type C, when equipped with separating recognizer families of sizes n and m, must satisfy n = m. Researchers constructing effective manifolds from recognition quotients cite it to guarantee that dimension is independent of the chosen refinement sequence. The declaration is a direct structural definition that packages the invariance condition as a Prop without further proof obligations.
Claim. Let $C$ be a type. The property DimensionInvariant$(C)$ holds when, for any two directed refinement systems sys$_1$ and sys$_2$ on $C$ that both satisfy RefinementConverges, and for any natural numbers $n$ and $m$ such that separating families of recognizers of cardinalities $n$ and $m$ exist, it follows that $n = m$.
background
DirectedRefinement packages a monotone sequence of recognizers indexed by the naturals, with each later recognizer strictly finer than the previous via IsFinerThan'. RefinementConverges requires that the sequence eventually separates every pair of distinct points in $C$: if two points remain indistinguishable at every stage, they must be identical. The module EffectiveManifoldTheory formalizes the structural hypotheses U1–U4 needed for an effective manifold; U3 is the statement that dimension is invariant under choice of convergent refinement sequence.
proof idea
This is a structural definition that directly encodes the invariance statement as a universal quantification over pairs of convergent systems and their separation counts; no lemmas are applied and no tactics are used.
why it matters
The declaration records the U3 hypothesis interface inside the EffectiveManifold bundle, which the status_summary treats as one of the four open problems whose conjunction yields the U1 data structure. It supports the Recognition Science claim that spatial dimension arises uniquely from the forcing chain once convergence and non-collapse are secured, and it is referenced by the downstream status summary that tracks formalization progress on U1–U4.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.