twoOrbit_toNat

In the Primitive Recognition Calculus, distinction orbits are an inductive copy of the naturals: zero is the identity position and succ steps once along the orbit. The verifier map toNat simply counts those steps, sending zero to 0 and succ n to the successor of the count of n. The two-step orbit is defined as the successor of the unit orbit, so it is the second nonzero position on that chain.

This module builds the rational J-cost objects used by PRC: ratio orbits with numerator and denominator drawn from signed distinction orbits, then mapped to rationals and reals. The constant 2 is the first nontrivial calibration point for those ratio objects and for later prime-direction uniqueness arguments. Upstream arithmetic-from-logic supplies the same iteration-count reading on the pure logic naturals; here the orbit-level map is the one that appears in simp lemmas.

One-line definitional proof. Unfolding the two-step orbit as succ of one, and one as succ of zero, the recursive clauses of the orbit-to-Nat map yield Nat.succ (Nat.succ 0), which is definitionally 2, so rfl closes the goal. Marked @[simp] so downstream ratio-to-rational lemmas can discharge the denominator or numerator count automatically.

This is the base numeric anchor for PRC's ratio-orbit calculus. It feeds the simp proofs that the ratio orbit two evaluates to the rational 2 and that half evaluates to 1/2, which in turn supply the two-point calibration used by character-pair cost consistency. Downstream uniqueness results use it to separate three from two by comparing Nat images, to identify the two-orbit as a prime orbit, and to show that every other prime direction has 2-adic valuation zero on its rational image. In the broader Recognition chain this is scaffolding for native cost uniqueness and for the transport that turns a single two-calibration plus prime-pair products into calibration on every native prime axis, not a T5–T8 landmark itself.