 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. -/
 136theorem sign_distinguishes_3_neg3 : ¬Indistinguishable signRecognizer 3 (-3) := by
 137  simp [Indistinguishable, signRecognizer, signOf]
 138
 139theorem magnitude_indist_3_neg3 : Indistinguishable magnitudeRecognizer 3 (-3) := by
 140  simp [Indistinguishable, magnitudeRecognizer]
 141
 142theorem sign_indist_3_5 : Indistinguishable signRecognizer 3 5 := by

papers checked against this theorem

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