DirectedRefinement

formal source

  54/-! ## U2: Refinement Convergence -/
  55
  56/-- A directed system of recognizers indexed by ℕ, ordered by refinement. -/
  57structure DirectedRefinement (C : Type*) where
  58  EventType : ℕ → Type*
  59  recognizer : (i : ℕ) → Recognizer C (EventType i)
  60  refines : ∀ i : ℕ, IsFinerThan' (recognizer (i + 1)) (recognizer i)
  61
  62/-- The refinement is monotone: later recognizers are always finer. -/
  63theorem DirectedRefinement.monotone_refines (sys : DirectedRefinement C)
  64    {i j : ℕ} (hij : i ≤ j) :
  65    IsFinerThan' (sys.recognizer j) (sys.recognizer i) := by
  66  induction hij with
  67  | refl => exact isFinerThan'_refl _
  68  | step _ ih =>
  69    exact isFinerThan'_trans _ _ _ (sys.refines _) ih
  70
  71/-- U2: The convergence condition for a directed refinement system.
  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)