RefinementConverges

formal source

  72The refinement eventually separates any two distinguishable points:
  73for any c₁ ≠ c₂ in C, there exists an index i such that R_i
  74distinguishes them. -/
  75structure RefinementConverges (sys : DirectedRefinement C) : Prop where
  76  eventually_separates : ∀ c₁ c₂ : C,
  77    (∀ i, Indistinguishable (sys.recognizer i) c₁ c₂) → c₁ = c₂
  78
  79/-! ## U3: Dimension Invariance -/
  80
  81/-- U3: Dimension invariance under refinement choice.
  82Two directed refinement systems that both converge and both admit
  83a common separation count produce the same dimension.
  84(The full statement requires chart-atlas infrastructure; here we
  85record it as a property of the separating-recognizer count.) -/
  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. -/
 100structure NonCollapseCondition (sys : DirectedRefinement C) : Prop where
 101  nontrivial_at_all_stages : ∀ i : ℕ,
 102    ∃ c₁ c₂ : C, ¬Indistinguishable (sys.recognizer i) c₁ c₂
 103  monotone_separation : ∀ i : ℕ, ∀ c₁ c₂ : C,
 104    ¬Indistinguishable (sys.recognizer i) c₁ c₂ →
 105    ¬Indistinguishable (sys.recognizer (i + 1)) c₁ c₂