theorem
proved
discrete_indist_iff_eq
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RecogGeom.Examples on GitHub at line 47.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
70
71/-- Sign is nonempty -/
72instance : Nonempty Sign := ⟨Sign.zero⟩
73
74/-- The sign function -/
75def signOf : ℤ → Sign
76 | n => if n < 0 then Sign.neg else if n = 0 then Sign.zero else Sign.pos
77