induction
plain-language theorem explainer
Structural induction on the distinction orbit: any property true at zero and closed under successor holds for every orbit element. Cited when proving facts about the base-neutral δ-orbit without switching to Lean Nat. The proof is ordinary inductive elimination on the inductive type.
Claim. Let $P$ be any predicate on the distinction naturals (the base-neutral finite orbit of repeated distinction). If $P(0)$ holds and $\forall n,\, P(n)\Rightarrow P(n+1)$, then $P(n)$ holds for every distinction natural $n$.
background
DistinctionNat is the inductive type with constructors zero and succ, documented as the base-neutral finite orbit of repeated distinction (K2.12). It is the δ-orbit object of the Primitive Recognition Calculus: each successor is one more application of distinction, with no preferred radix.
The surrounding module builds the Peano package on this orbit (zero ≠ succ, succ injective, induction, and the Nat bridge via toNat/ofNat). The pattern matches ArithmeticFromLogic, where successor is one more application of a generator and the Peano axioms are theorems of the inductive structure rather than postulates.
R8 is the induction clause of that package: the elimination principle that lets one prove orbit-wide statements from a base case and a successor step.
proof idea
Standard structural induction on DistinctionNat. Introduce an arbitrary n, then induct on n. The zero branch returns the given base hypothesis. The succ branch feeds the inductive hypothesis into the given successor-closure hypothesis. No auxiliary lemmas are required; the proof is the built-in eliminator of the inductive type.
why it matters
R8 completes the Peano triad on the δ-orbit together with zero_ne_succ and succ_injective. Without induction, orbit-wide statements (cost recurrence, rung counting, ladder identities) cannot be discharged inside the recognition calculus.
In the broader RS foundation this is the arithmetic engine behind the phi-ladder and eight-tick bookkeeping: once the orbit carries induction, finite counts of distinction steps become ordinary inductive arguments rather than external Nat appeals. Downstream Nat isomorphism lemmas (toNat, ofNat and their round-trips) sit on the same inductive spine.
No parent theorems currently list this declaration as a dependency in the graph, so it is infrastructure waiting on orbit-level proofs rather than a leaf of a named forcing step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.