zero_ne_succ
plain-language theorem explainer
Zero is never a successor in the distinction-orbit naturals: for every n, 0 ≠ S(n). Anyone assembling Peano structure, Lawvere NNOs, or logic realizations from the primitive recognition calculus cites this as axiom R8 / Peano P1. The proof is pure constructor discrimination: assume equality and case-split.
Claim. Let $\mathrm{DN}$ be the inductive type of distinction-orbit naturals with constructors $0$ and $S$. Then for every $n \in \mathrm{DN}$, $0 \neq S(n)$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with constructors zero and succ, the recognition-calculus stand-in for the natural numbers before any base or metric is chosen.
In the ArithmeticFromLogic layer the same statement appears as Peano P1: "the identity is distinguishable from any iterate of the generator." Here it is restated on the orbit type itself so that orbit-level lemmas (injectivity of successor, induction, the toNat/ofNat isomorphism) can quote a local fact rather than reach across modules.
The surrounding module develops the Peano package for this orbit: zero ≠ succ, succ injective, induction, and the mutually inverse maps to ordinary Nat.
proof idea
Assume h : zero = succ n. The tactic cases h exhausts constructors of the equality type; no case is inhabited because zero and succ are distinct constructors of the inductive type. Same one-step pattern as the LogicNat Peano P1 proof upstream.
why it matters
R8 is the first Peano axiom discharged as a theorem of the inductive orbit, not posited. Downstream it underwrites nontriviality of the canonical Lawvere NNO (logicNatNNO), the categorical and modular logic realizations, ordered and discrete realizations, and faithfulness of positive-ratio arithmetic interpretations. Without zero ≠ succ the carrier collapses and cost/compare structure cannot separate the identity from generator iterates. It sits at the foundation end of the forcing chain: arithmetic extracted from recognition before J-cost, φ, or the eight-tick octave appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.