Canonical +1 and -1 · genuine signed products · constructive solutions

Actual signed units and affine equations

Classify every actual signed product equal to one and solve the affine equation needed for finite inversion.

9 kernel- and Lean-verified Alpha-closed theorems · 4 conservative definitions · 2 notation dependencies

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

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

13 items
ZU0001 dirichlet_signed_unit_self_product

Each of the two canonical signed units has an actual signed square equal to positive one.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
ZU0002 dirichlet_signed_unit_product_classification

An actual signed product is positive one only for the two equal canonical units; mixed signs are constructively impossible.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
ZU0003 dirichlet_signed_unit_inverse_iff

The finite signed-unit predicate is equivalent to existence of an actual signed multiplicative inverse, not defined by an inverse oracle.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
ZU0004 dirichlet_signed_add_cancel_left

Cancellation of a common canonical signed summand follows by constructing its actual additive inverse.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
ZU0005 dirichlet_signed_add_solve

Construct the signed addend taking any canonical signed r to any canonical signed e, including zero and negative values.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
ZU0007 dirichlet_signed_unit_multiply_cancel_right

An actual signed unit can be cancelled from a common right factor without cancelling arbitrary zero or nonunit factors.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
ZU0008 dirichlet_signed_unit_affine_solve

Given either actual signed unit, construct both x and its actual product y with r+y=e; no difference, product or solution witness is supplied.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
ZU0009 dirichlet_signed_unit_affine_unique

Any two witnessed solutions of the same unit-affine equation have equal canonical inputs and equal actual product outputs.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
ND0142 SignedDecode(z,p,n)

The original canonical integer code: even 2p denotes p, and odd 2k+1 denotes −(k+1). The decoded positive and negative parts are normalized.

Conservative definition · notation layer 0
ND0145 SignedMul(a,b,c)

Actual multiplication of original canonical signed codes; opposite-sign products remain on the negative side of the balance.

Conservative definition · notation layer 1
ND0144 SignedAdd(a,b,c)

Actual addition of original canonical signed codes, witnessed by their decoders and balanced equality.

Conservative definition · notation layer 1
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 definition · notation layer 0

Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.