ofNat
plain-language theorem explainer
Recursive embedding of ordinary natural numbers into the base-neutral distinction orbit: zero maps to the orbit origin and successor maps to orbit successor. Anyone building integer bridges, delta certificates, or chart transitions from verifier Nats cites this. The body is the standard structural recursion on Nat.
Claim. Define a map $\mathrm{ofNat}:\mathbb{N}\to\mathrm{DistinctionNat}$ by $\mathrm{ofNat}(0)=\mathbf{0}$ and $\mathrm{ofNat}(n+1)=S(\mathrm{ofNat}(n))$, where $S$ is the orbit successor and $\mathbf{0}$ is the orbit origin.
background
DistinctionNat (K2.12) is the inductive type of finite orbit positions under repeated distinction: a zero constructor and a successor constructor. It is deliberately base-neutral: it records only how many distinction steps have been taken, not a preferred radix.
The surrounding Orbit module develops Peano-style structure on this type (zero not a successor, successor injective, induction) together with the inverse extraction toNat. The present map is the canonical section that places a verifier natural number onto that orbit.
Upstream, the same successor pattern appears in ArithmeticFromLogic as one more application of a generator on LogicNat; the Orbit version is the recognition-calculus counterpart used when positions, not abstract Peano numerals, are the objects of interest.
proof idea
Definition by structural recursion on Nat. The zero case returns the orbit zero constructor. The successor case applies the orbit successor to the recursively computed image. No lemmas are invoked; the equation compiler supplies the recursor.
why it matters
This is the standard entry point from Lean's built-in naturals into the recognition orbit. Downstream it feeds the integer bridge (fromInt, fromInt_toInt, toInt_fromInt in IntegersFromLogic), the explicit $\mathbb{Z}\to\mathbb{N}$ certificate and its injectivity in DeltaForced, chart-transition certificates and magnitude underdetermination in Factorization.ChartTransition, and length-counting arguments on closed surface-type classifications in cosmology.
In the Recognition framework it is scaffolding for the primitive recognition calculus: once Nats sit on the distinction orbit, forced delta structure, rung arithmetic, and later mass/ladder constructions can treat verifier counts as orbit positions rather than bare numerals. It does not itself force phi, the eight-tick octave, or $D=3$; those live higher in the T0–T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.