signRecognizer
plain-language theorem explainer
The signRecognizer is the Recognizer structure on the integers whose recognition map sends each integer to one of three sign categories. Researchers building concrete models of recognition geometry cite this as the canonical finite-class example on ℤ. The definition is a direct instantiation of the Recognizer type with the signOf map together with a one-line nontriviality witness.
Claim. Let Sign be the three-element type with constructors neg, zero, pos. The sign recognizer is the Recognizer(ℤ, Sign) whose recognition map R is the function signOf : ℤ → Sign that returns neg on negative inputs, zero on zero, and pos on positive inputs.
background
The module supplies concrete recognition geometries to illustrate the general framework. Sign is the inductive type with three constructors neg, zero, pos. The function signOf maps each integer to its sign category, producing exactly three equivalence classes under the induced indistinguishability relation. The upstream signOf definition supplies the concrete map used here; the nontrivial instance from KinshipGraphCohomology is referenced only for the Nonempty requirement on the target type.
proof idea
The definition is a one-line wrapper that sets the recognition map R to signOf. The nontrivial field is discharged by exhibiting the pair -1 and 1 and simplifying with the definition of signOf.
why it matters
This definition supplies the concrete instance used by every subsequent theorem in the module, including composition_refines (which shows sign and magnitude together refine partitions), sign_indistinguishable (which equates indistinguishability with equal signs), and the various neg_indist and sign_distinguishes_3_neg3 lemmas. It demonstrates a recognizer with finitely many classes (three) and serves as the running example for the composition principle in the Recognition Geometry section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.