def
definition
discreteRecognizer
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogGeom.Examples on GitHub at line 39.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
66 | neg : Sign
67 | zero : Sign
68 | pos : Sign
69 deriving DecidableEq, Repr