Sign
plain-language theorem explainer
Defines the three-valued sign type with negative, zero, and positive elements. Researchers building sign recognizers on the integers cite it to establish the three equivalence classes in the quotient. The construction is a direct inductive definition deriving decidable equality and a nonempty instance.
Claim. Let $S = T$ be the type whose elements are the three labels negative, zero, and positive, equipped with decidable equality.
background
The Recognition Geometry module supplies concrete examples that illustrate the overall framework. One such example is the sign recognizer on the integers, which partitions them into exactly three equivalence classes. The type supplies the codomain for that recognizer. Upstream negation definitions in integers, rationals, and elliptic curves supply the algebraic operations that the sign distinction refines.
proof idea
The declaration is an inductive definition that introduces the three constructors directly. A separate instance then witnesses nonemptiness by exhibiting the zero constructor. No lemmas or tactics are invoked.
why it matters
The type anchors the sign-recognizer example, which demonstrates that the integer quotient under sign equivalence contains precisely three classes. It is invoked by downstream results on electron affinity for halogens and argon, banding falsifiers in flight, coherence gates in gravity candidates, and axis and sign-flip counts in the D3 gauge construction. It thereby supplies the discrete three-class partition required for the composition-refinement statements that follow in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.