ofNat_succ
plain-language theorem explainer
Converting the successor of a natural number into a distinction-orbit position equals applying the orbit successor to the converted number. Anyone proving Nat ↔ δ-orbit transport or simplifying mixed Nat/orbit expressions cites this simp lemma. The equality is definitional: it unfolds the recursive clause of the embedding and closes by reflexivity.
Claim. For every natural number $n$, embedding $n+1$ into the distinction orbit equals the orbit successor of the embedding of $n$: $\mathrm{ofNat}(n+1)=\mathrm{succ}(\mathrm{ofNat}(n))$.
background
In the primitive recognition calculus, distinction-orbit positions (DistinctionNat) carry a Peano structure whose successor is one further application of the generator along the δ-orbit. Lean Nat is the verifier side; the embedding ofNat : Nat → DistinctionNat is defined by recursion: zero maps to the orbit zero, and Nat.succ n maps to succ (ofNat n).
Upstream, successor on the logic/orbit side is exactly that generator step (ArithmeticFromLogic: "Successor is one more application of the generator"). The surrounding Orbit module builds the two-way transport between verifier naturals and orbit positions so that arithmetic forced from recognition matches ordinary Nat.
This lemma is the successor half of that embedding's computational interface; the zero case is the sibling ofNat_zero.
proof idea
One-line definitional proof. Unfolding ofNat on Nat.succ n yields exactly succ (ofNat n) by the second clause of the recursive definition, so rfl closes. Marked @[simp] for automatic rewriting in mixed Nat/orbit goals.
why it matters
Sits in the Foundation layer that derives Peano arithmetic from recognition structure rather than positing it. Together with ofNat_zero, toNat_succ, and the round-trip lemmas (toNat_ofNat, ofNat_toNat), it underwrites the K4.5 claim that transport from Lean Nat to the δ-orbit and back is the identity. That transport is the structural witness that abstract Peano structure is the orbit of a non-trivial generator under multiplication (ArithmeticFromLogic embedding into positive reals). No downstream uses are recorded yet; the lemma is infrastructure for those round-trips and for any later forcing-chain step that needs to move induction or counting between verifier Nat and orbit positions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.