toNat
plain-language theorem explainer
Structural map from the base-neutral finite orbit of repeated distinction to ordinary natural numbers: origin goes to 0, each successor adds one. Anyone bridging RS orbit positions into Lean arithmetic or integer exponents cites it. The body is bare recursive pattern-match on the inductive constructors.
Claim. Define a verifier map from the base-neutral finite orbit of repeated distinction into $\mathbb{N}$ by sending the orbit origin to $0$ and each successor step $n$ to $\mathrm{toNat}(n)+1$.
background
In the Primitive Recognition Calculus, DistinctionNat (K2.12) is the inductive type of finite orbits generated by repeated distinction: a zero constructor and a unary successor. It is base-neutral, i.e. it records only iteration count, not a preferred radix. The module builds Peano-style structure on that type (zero ≠ succ, succ injective, induction) before exporting a verifier representation.
The same pattern already appears for LogicNat in ArithmeticFromLogic, where toNat is documented as "the forward map: read off the iteration count." Here the target is Lean's built-in Nat, so downstream code can reuse ordinary arithmetic, integer casts, and Mathlib lemmas without redeveloping them on the orbit type.
Local setting is the orbit layer of the foundation stack: distinction orbits feed cost characters, gauge classification, and the φ-ladder once positions are readable as naturals.
proof idea
Not a proof: a definition by structural recursion. Match on the two constructors of the orbit type; send zero to 0 and succ n to Nat.succ of the recursive image. No lemmas are invoked; the equation compiler supplies the recursor.
why it matters
This is the standard bridge from RS orbit positions into ordinary natural-number arithmetic. Downstream uses are broad: φ-powers on the φ-ladder (phiPow), lattice-energy proxies that cast charges via toNat, gauge-orbit character evaluation at positive rationals (char_at_pos), rational-trace exponent theorems that extract positive integer exponents, and cancellation lemmas back in ArithmeticFromLogic.
In the Recognition framework it sits under the early foundation (distinction → orbit → arithmetic), before T5–T8 forcing. Without a verifier map, orbit indices cannot enter cost factorizations or the integer half of the signed-power family results. Sibling lemmas (toNat_zero, toNat_succ, toNat_ofNat, ofNat_toNat) close the isomorphism; this declaration only supplies the forward leg.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.