sign_distinguishes_3_neg3
plain-language theorem explainer
Sign recognizer on the integers distinguishes 3 from -3 because they map to distinct events under the sign map. Researchers constructing recognition geometries cite this example to show how sign partitions separate positives from negatives where magnitude alone collapses them. The argument is a direct simplification that unfolds indistinguishability and the sign assignment.
Claim. $¬(3 ∼_{sign} (-3))$, where $∼_{sign}$ is indistinguishability under the recognizer whose event map sends each integer to its sign (negative if less than zero, zero if equal to zero, positive otherwise).
background
The Recognition Geometry module supplies concrete examples on finite sets and on ℤ. The Sign type is the three-element inductive type with constructors negative, zero, and positive. The signOf function maps an integer n to negative when n < 0, to zero when n = 0, and to positive otherwise. The signRecognizer packages this map as a Recognizer ℤ Sign. Indistinguishability under any recognizer holds precisely when two configurations produce identical events under the recognizer's event map.
proof idea
One-line wrapper that applies simp with the definitions of Indistinguishable, signRecognizer, and signOf. The tactic reduces the negated equality of sign events for 3 and -3 to the immediate observation that positive differs from negative.
why it matters
The result feeds the examples_status definition, which records that sign and magnitude together refine the partition beyond either recognizer alone. It supplies the concrete observation, stated in the module documentation, that sign separates 3 from -3 while magnitude does not. The example illustrates the composition principle within the Recognition Geometry setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.