finConfigSpace

formal source

  32/-! ## Example 1: Discrete Recognition on Fin n -/
  33
  34/-- Configuration space: Fin n (n ≥ 2 distinct configurations) -/
  35instance finConfigSpace (n : ℕ) [h : NeZero n] : ConfigSpace (Fin n) where
  36  nonempty := ⟨0⟩
  37
  38/-- The discrete recognizer: identity map (distinguishes everything) -/
  39def discreteRecognizer (n : ℕ) [h : NeZero n] (hn : 2 ≤ n) :
  40    Recognizer (Fin n) (Fin n) where
  41  R := id
  42  nontrivial := by
  43    use ⟨0, by omega⟩, ⟨1, by omega⟩
  44    simp [Fin.ext_iff]
  45
  46/-- **Theorem**: Discrete recognizer - indistinguishable iff equal -/
  47theorem discrete_indist_iff_eq (n : ℕ) [h : NeZero n] (hn : 2 ≤ n)
  48    (c₁ c₂ : Fin n) :
  49    Indistinguishable (discreteRecognizer n hn) c₁ c₂ ↔ c₁ = c₂ := by
  50  simp [Indistinguishable, discreteRecognizer]
  51
  52/-- **Corollary**: Each config is in its own resolution cell -/
  53theorem discrete_singleton_cells (n : ℕ) [h : NeZero n] (hn : 2 ≤ n) (c : Fin n) :
  54    ResolutionCell (discreteRecognizer n hn) c = {c} := by
  55  ext x
  56  simp [ResolutionCell, discrete_indist_iff_eq]
  57
  58/-! ## Example 2: Sign Recognizer on ℤ -/
  59
  60/-- Integer configuration space -/
  61instance : ConfigSpace ℤ where
  62  nonempty := ⟨0⟩
  63
  64/-- Three-valued sign type -/
  65inductive Sign : Type