signRecognizer
plain-language theorem explainer
The signRecognizer constructs a Recognizer on the integers with codomain the three-element Sign type by setting its recognition map to the signOf function. Researchers studying concrete recognition geometries cite it as the standard example yielding exactly three equivalence classes on ℤ. The definition is a direct construction that also proves non-triviality by exhibiting -1 and 1 as witnesses with distinct images under signOf.
Claim. The sign recognizer is the structure Recognizer on ℤ with output type Sign (the inductive type with constructors neg, zero, pos) whose recognition map is the function signOf that sends n to neg when n < 0, to zero when n = 0, and to pos otherwise.
background
The Recognition Geometry module supplies concrete examples that illustrate the abstract framework. The Sign type is the three-valued inductive type with constructors neg, zero, pos. The signOf function maps each integer to its sign class according to the rule: negative for n < 0, zero for n = 0, positive otherwise. This yields the quotient ℤ/~ with exactly three classes, in contrast to the discrete recognizer (quotient isomorphic to the original space) and the magnitude recognizer (infinitely many classes).
proof idea
The definition directly sets the R field of the Recognizer structure to signOf. The nontrivial field is discharged by the tactic use -1, 1 followed by simp [signOf], which reduces the goal to showing that signOf(-1) ≠ signOf(1).
why it matters
This supplies the canonical three-class example on ℤ that is referenced by downstream results including sign_indistinguishable (two integers are indistinguishable under the recognizer precisely when signOf n = signOf m) and composition_refines (sign and magnitude together distinguish more pairs than either alone). It demonstrates the module insight that the sign recognizer partitions ℤ into neg, zero, pos classes and serves as the base for theorems on indistinguishability and refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.