toNat_succ
plain-language theorem explainer
The verifier map from distinction orbits to ordinary naturals intertwines successor with Nat.succ. Anyone proving arithmetic recovery or order facts on DistinctionNat cites this simp lemma. The proof is definitional reflexivity from the recursive clause of toNat.
Claim. For every finite distinction orbit $n$, the verifier natural of the successor orbit equals the ordinary successor of the verifier natural of $n$: $\mathrm{toNat}(\mathrm{succ}\, n) = \mathrm{succ}(\mathrm{toNat}\, n)$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with constructors zero and succ, the pure Peano spine without a preferred radix. It is the orbit-side twin of LogicNat in ArithmeticFromLogic.
The map toNat is the verifier representation of an orbit as a Lean Nat: zero maps to 0 and succ n maps to Nat.succ (toNat n). Its inverse ofNat rebuilds the orbit by iterating succ. The parallel statement for LogicNat is already recorded as ArithmeticFromLogic.toNat_succ, with the same definitional shape.
Locally this sits in PrimitiveRecognitionCalculus.Orbit, where the orbit is treated as the primitive counting object before arithmetic operations are recovered.
proof idea
One-line definitional proof: rfl. Unfolding toNat on the constructor succ n yields Nat.succ (toNat n) by the second equation of the recursive definition, so both sides are identical terms.
why it matters
This simp fact is the successor half of the orbit–Nat equivalence. Downstream it feeds recovery and order lemmas in ArithmeticFromLogic: fromNat_toNat and toNat_fromNat (round-trip), toNat_add and toNat_mul (operation recovery), and order transport such as toNat_lt, lt_irrefl, and lt_iff_le_and_ne, which rewrite through toNat_succ when comparing successors.
In the Recognition stack it anchors the claim that Peano structure is not posited but read off the inductive orbit of distinction. It is scaffolding for the arithmetic layer that later supports mass ladders and tick counting, not a physics law itself. Sibling lemmas toNat_zero, ofNat_succ, and ofNat_toNat complete the same dictionary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.