succ_injective
plain-language theorem explainer
Successor on the δ-orbit is injective: equal successors force equal predecessors. Anyone assembling Peano structure from the primitive recognition orbit cites this as R8. The proof is pure constructor case-split on the inductive step equality, then reflexivity.
Claim. The successor map on the distinction orbit is injective: whenever $\mathrm{succ}(a)=\mathrm{succ}(b)$, one has $a=b$.
background
In the primitive recognition calculus, the δ-orbit is the free inductive chain generated by repeated application of a single generator step from a base point. The local type (sibling DistinctionNat) is that orbit; its constructor package is the usual zero-plus-step shape.
Successor is defined as one more application of the generator (parallel to ArithmeticFromLogic: "Successor is one more application of the generator"). Injectivity of that map is Peano's second axiom, here labeled R8, and is not postulated: it is read off constructor disjointness of the inductive type.
The same fact appears upstream as Peano P2 in ArithmeticFromLogic, with the gloss that constructor disjointness "reflects the injectivity of multiplication by the generator on the orbit." Sibling companions are zero-not-successor and induction over the δ-orbit.
proof idea
Term/tactic hybrid, four lines. Introduce predecessors $a,b$ and the equality hypothesis $h:\mathrm{succ},a=\mathrm{succ},b$. Case-split on $h$: because successor is the inductive .step constructor, the only way two steps can be equal is if their arguments are definitionally equal. Close with reflexivity. No external lemmas are required; the argument is pure inductive-constructor injectivity.
why it matters
R8 is one of the Peano axioms forced as a theorem from the recognition orbit rather than assumed. Downstream it supplies the step_injective field of the Peano surface on the canonical arithmetic object (canonical_peanoSurface), and is consumed across the LogicRealization stack: categorical NNO realization, discrete bool realization, modular cyclic realization, ordered nat realization, physics realization, and positive-ratio comparison embeddings.
Together with zero-not-successor and induction, it closes the arithmetic surface that later layers treat as the discrete carrier for cost comparison. In the broader RS forcing picture this is the arithmetic half of reading structure off the generator orbit, before constants and continuum geometry are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.