neg_pos_dist

formal source

  92  simp [Indistinguishable, signRecognizer, signOf]
  93
  94/-- **Theorem**: -1 ≁ 1 (different signs) -/
  95theorem neg_pos_dist : ¬Indistinguishable signRecognizer (-1) 1 := by
  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