theorem
proved
term proof
diff_magnitude_dist
show as:
view Lean formalization →
formal statement (Lean)
121theorem diff_magnitude_dist : ¬Indistinguishable magnitudeRecognizer 2 3 := by
proof body
Term-mode proof.
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. -/