 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)
 130    - Magnitude alone: 3 ~ -3 (both have magnitude 3)
 131
 132    So sign distinguishes 3 from -3, but magnitude doesn't.
 133    Conversely, magnitude distinguishes 3 from 5, both positive.
 134
 135    The composition (sign, magnitude) distinguishes both. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.