signRecognizer
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not claim this is the unique recognizer on ℤ.
- Does not extend the construction to other base types or continuous domains.
- Does not derive physical constants or dimensions from this example.
- Does not address composition with recognizers outside the module.
formal statement (Lean)
79def signRecognizer : Recognizer ℤ Sign where
80 R := signOf
proof body
Definition body.
81 nontrivial := by
82 use -1, 1
83 simp [signOf]
84
85/-- **Theorem**: Two integers are indistinguishable iff same sign -/