DimensionInvariant
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not supply the chart-atlas infrastructure required for the full manifold statement.
- Does not prove that a well-defined separation count exists for a given system.
- Does not derive invariance from the Recognition Composition Law or the phi-ladder.
- Does not address the non-collapse condition formalized in NonCollapseCondition.
formal statement (Lean)
86structure DimensionInvariant (C : Type*) : Prop where
87 invariant : ∀ (sys₁ sys₂ : DirectedRefinement C)
88 (hconv₁ : RefinementConverges sys₁)
89 (hconv₂ : RefinementConverges sys₂)
90 {n m : ℕ}
91 (hsep₁ : ∃ (Es : Fin n → Type*) (rs : (i : Fin n) → Recognizer C (Es i)), True)
92 (hsep₂ : ∃ (Es : Fin m → Type*) (rs : (i : Fin m) → Recognizer C (Es i)), True),
93 n = m
94
95/-! ## U4: Non-Collapse Condition -/
96
97/-- U4: The refinement does not collapse: at every stage, the quotient
98has at least as many classes as the previous stage (monotone cardinality).
99This prevents dimension from dropping. -/