one

In the Primitive Recognition Calculus, integers are not postulated; they are recovered from signed orbit differences. A signed orbit is a pair of distinction naturals (pos, neg) whose intended meaning is the difference pos - neg (K4.6). Distinction naturals themselves come from the logic-level Peano structure: zero is the identity, and successor is one more application of the generator.

This module sits after orbit arithmetic and builds the displays that later quotient to PRC integers and rationals. The zero signed orbit is the balanced pair (0,0); the unit is the next canonical display, with positive leg one and negative leg zero. Upstream, succ is defined as .step n, and Peano P1 (zero ≠ succ n) guarantees the unit is distinguishable from zero at the display level before any quotient.

Pure definitional constructor: pack DistinctionNat.succ DistinctionNat.zero into the positive field and DistinctionNat.zero into the negative field of SignedOrbit. No lemmas are applied; the term is the pair itself.

Gives the canonical +1 display inside the signed-orbit layer that feeds K4.8 PRC integers (PRCInt as the quotient of signed orbits by balanced-length) and, via numerators, K4.7–K4.8 ratio orbits and PRC rationals. Without a named unit, integer and rational constructors would repeatedly inline succ zero, obscuring the arithmetic ladder that later connects to the forcing chain and mass/yardstick constructions. No downstream uses are wired in the current graph, so this is infrastructure rather than a cited lemma; it closes the zero/one pair beside zero and zero_toInt in the same namespace.