ND0313

SignedUnit(u)

Exactly the canonical signed codes 2 (+1) and 1 (-1). Its equivalence with an actual signed multiplicative inverse and the affine-equation solver are separately proved, not assumed by this two-case graph.

Conservative notation; not a theorem, primitive, or axiom.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Definition in prerequisite notation

u = 2 ∨ u = 1

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
(((u)) = 2 \/ ((u)) = 1)

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

none — first-order arithmetic only

Definitions depending on this notation

none

Checked theorems using this definition

ZU0001 · dirichlet_signed_unit_self_productZU0003 · dirichlet_signed_unit_inverse_iffZU0006 · dirichlet_signed_unit_multiply_involutionZU0007 · dirichlet_signed_unit_multiply_cancel_rightZU0008 · dirichlet_signed_unit_affine_solveZU0009 · dirichlet_signed_unit_affine_unique