plus_minus_indist

formal source

 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
 143  simp [Indistinguishable, signRecognizer, signOf]
 144
 145theorem magnitude_distinguishes_3_5 : ¬Indistinguishable magnitudeRecognizer 3 5 := by
 146  simp [Indistinguishable, magnitudeRecognizer]
 147