orbit_succ_ne_zero
plain-language theorem explainer
For any finite distinction-orbit index, its successor is never the zero orbit. Downstream PRC native-cost uniqueness proofs cite this whenever they build an orbit direction at a successor step. The argument is a one-line symmetry of the Peano fact that zero is not a successor on DistinctionNat.
Claim. For every finite distinction-orbit index $p$, $\mathrm{succ}(p) \neq 0$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with constructors zero and successor. Orbit directions and ratio characters are only defined on nonzero indices, so successor steps must be certified nonzero before those maps apply.
Upstream, R8 states the Peano axiom that zero is not a successor: for every $n$, $0 \neq \mathrm{succ}(n)$. The same fact appears for the logic-native naturals in ArithmeticFromLogic (Peano P1: the identity is distinguishable from any iterate of the generator). The present lemma is the orientation needed at call sites that already hold a successor and must discharge a nonzero hypothesis.
proof idea
Assume for contradiction that $\mathrm{succ}(p) = 0$. Symmetry of equality yields $0 = \mathrm{succ}(p)$, which is exactly the negation of DistinctionNat.zero_ne_succ p. That contradiction closes the proof. No induction or arithmetic beyond the inductive constructors is used.
why it matters
Native-cost uniqueness for PRC characters works by transporting identity orientation along the distinction orbit. Almost every successor-step interface in this module threads this lemma as the nonzero certificate at $\mathrm{succ}(p)$: the forward and backward one-step identity laws (PRCCharacterOrbitIdentityExtendsSuccessorStep, PRCCharacterOrbitIdentityContractsSuccessorStep), the additive cross-equation for orbit direction at a successor, successor-respect and additive-compatibility statements, and the prime-floor transport theorems that rebuild identity from the unit.
Without a uniform nonzero fact at successors, orbit-direction characters could not be evaluated on the inductive spine, and the doubled-trace / d'Alembert route from ratio characters to the unique native cost would stall. The lemma is pure Peano bookkeeping inside the foundation layer; it does not itself invoke J-cost uniqueness (T5) or $\varphi$, but it is load-bearing for the uniqueness pipeline that later pins the native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.