theorem
proved
zero_pos_dist
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 99.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
96 simp [Indistinguishable, signRecognizer, signOf]
97
98/-- **Theorem**: 0 ≁ 1 (different signs) -/
99theorem zero_pos_dist : ¬Indistinguishable signRecognizer 0 1 := by
100 simp [Indistinguishable, signRecognizer, signOf]
101
102/-! ## Example 3: Magnitude Recognizer on ℤ -/
103
104/-- The magnitude recognizer: n ↦ |n| -/
105def magnitudeRecognizer : Recognizer ℤ ℕ where
106 R := fun n => n.natAbs
107 nontrivial := by
108 use 0, 1
109 simp
110
111/-- **Theorem**: n ~ m iff |n| = |m| -/
112theorem magnitude_indistinguishable (n m : ℤ) :
113 Indistinguishable magnitudeRecognizer n m ↔ n.natAbs = m.natAbs := by
114 rfl
115
116/-- **Theorem**: 3 ~ -3 (same magnitude) -/
117theorem plus_minus_indist : Indistinguishable magnitudeRecognizer 3 (-3) := by
118 simp [Indistinguishable, magnitudeRecognizer]
119
120/-- **Theorem**: 2 ≁ 3 (different magnitudes) -/
121theorem diff_magnitude_dist : ¬Indistinguishable magnitudeRecognizer 2 3 := by
122 simp [Indistinguishable, magnitudeRecognizer]
123
124/-! ## Example 4: Composition Refines Both -/
125
126/-- **Key Observation**: Combining sign and magnitude gives a finer recognizer.
127
128 - Sign alone: 3 ~ -3 (both positive/negative)... wait, that's wrong
129 - Actually sign: 3 ≁ -3 (positive vs negative)