Sign
The Sign type enumerates a three-element classification for discrete recognition on the integers, with constructors for negative, zero, and positive values. Workers on sign recognizers, quotient geometries, or composition refinements in Recognition Science cite this when partitioning Z into equivalence classes or building magnitude examples. The construction is a direct inductive enumeration that derives decidable equality and a nonempty instance via the zero constructor.
claimLet $Sign$ be the inductive type with three constructors $neg$, $zero$, and $pos$, equipped with decidable equality and a canonical nonempty instance witnessed by $zero$.
background
The module develops concrete recognition geometries to illustrate the framework. One example is the sign recognizer on Z, which partitions the integers into exactly three equivalence classes corresponding to negative, zero, and positive values. A second example is the magnitude recognizer, which yields infinitely many classes indexed by absolute value. These sit alongside the discrete recognizer on finite sets, where the quotient recovers the original space exactly. The sign construction supplies the basic three-valued partition used in later composition and indistinguishability arguments.
proof idea
The declaration is an inductive definition that introduces the three constructors directly. It then derives DecidableEq and Repr instances automatically and supplies a Nonempty instance by exhibiting the zero constructor.
why it matters in Recognition Science
This definition anchors the sign-recognizer example that demonstrates Z/~ has precisely three classes, feeding the composition-refines result in the same module. Downstream it supports electron-affinity proxies for halogens and argon, axis-permutation and sign-flip counts in the D3 gauge group, banding falsifiers in flight models, and coherence-gate falsifiers in gravity candidates. It supplies the discrete three-valued structure that aligns with the eight-tick octave and sign-flip subgroups appearing in the D=3 gauge analysis.
scope and limits
- Does not define addition, multiplication, or any group law on Sign.
- Does not prove indistinguishability relations or quotient isomorphisms.
- Does not extend the type to real or continuous sign functions.
- Does not address decidability of predicates beyond the derived equality instance.
formal statement (Lean)
65inductive Sign : Type
66 | neg : Sign
67 | zero : Sign
68 | pos : Sign
69 deriving DecidableEq, Repr
70
71/-- Sign is nonempty -/
72instance : Nonempty Sign := ⟨Sign.zero⟩
proof body
Definition body.
73
74/-- The sign function -/