equivNat
plain-language theorem explainer
The finite δ-orbit of repeated distinction is type-equivalent to the natural numbers, via mutually inverse maps that count successors and rebuild orbits. Anyone moving Peano structure, countability, or verifier displays out of the primitive recognition calculus cites this bridge. The definition only packages the two already-proved round-trip identities into a single Equiv.
Claim. There is a type equivalence between the finite $\delta$-orbit of repeated distinction and $\mathbb{N}$: the forward map reads successor depth, the inverse rebuilds the orbit by iteration, and each composition is the identity.
background
In the Primitive Recognition Calculus, arithmetic is grown from distinction alone. The carrier DistinctionNat (K2.12) is the base-neutral finite orbit under repeated distinction: an inductive type with a zero and a successor, deliberately free of any preferred radix.
Two transport maps sit on that carrier. The forward map sends an orbit position to a verifier natural by counting successors; the inverse rebuilds an orbit by iterating successor from zero. Upstream lemmas already show both compositions are identity (K4.5 round-trips).
The local setting is the Orbit layer of Foundation: the same pattern appears for the logic-native Peano object in ArithmeticFromLogic, whose recovery theorem likewise packages round-trips into a carrier equivalence with Nat.
proof idea
Pure structure assembly, not a new argument. The equivalence is defined by taking the forward map to be the successor-counting display, the inverse to be the orbit-rebuilding map, the left inverse law to be the already-proved transport identity from orbit to Nat and back, and the right inverse law to be the dual identity. No tactics beyond filling those four fields.
why it matters
K4.5 in the PRC numbering: the δ-orbit is exactly Lean Nat as a verifier display. Downstream, the continuum-not-forced certificate uses this equivalence as the countable δ-index witness (delta_index_countable := ⟨DistinctionNat.equivNat⟩), so continuum cardinality is not forced by distinction. Distinction-to-arithmetic countability likewise routes through the parallel LogicNat recovery. Forced-integer injectivity and the forced-semiring identification with Nat lean on the same carrier bridge. The result is the clean hand-off from primitive distinction orbits to ordinary Peano arithmetic without smuggling continuum structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.