toNat_ofNat
plain-language theorem explainer
Round-tripping a natural number through the δ-orbit embedding and back recovers the original Nat. Anyone transporting classical arithmetic (totients, primes, Euler exponents) into DistinctionNat cites this identity. The proof is a short induction on n, with the successor step discharged by simp on the recursive clauses of ofNat.
Claim. For every $n \in \mathbb{N}$, reading the iteration count of the $\delta$-orbit built by iterating the successor $n$ times returns $n$: $\mathrm{toNat}(\mathrm{ofNat}(n)) = n$.
background
In PrimitiveRecognitionCalculus.Orbit, DistinctionNat is the native δ-orbit: the free inductive type generated by zero and a single successor step, the same Peano skeleton that ArithmeticFromLogic builds as LogicNat. The forward readout toNat counts how many steps separate a point from the identity; the inverse ofNat rebuilds that point by iterating the step from zero.
Upstream, ArithmeticFromLogic records the same pair on LogicNat: toNat is "the forward map: read off the iteration count," and successor is "one more application of the generator." The present module re-hosts that transport on DistinctionNat so later factorization and signed-orbit work can move freely between Lean Nat and the δ layer.
K4.5 packages the two directions of the isomorphism. This half is Nat → δ → Nat; the sibling ofNat_toNat is the converse.
proof idea
Induction on n : Nat.
- Zero case: both sides reduce by the base clauses of
ofNatandtoNat, sorflcloses. - Successor case: unfold
ofNat (n+1)tosucc (ofNat n), apply the inductive hypothesistoNat (ofNat n) = n, andsimp [ofNat, ih]finishes via the recursive clause oftoNatonsucc.
No external lemmas beyond the defining equations of ofNat/toNat and the induction principle on Nat.
why it matters
This is the workhorse rewrite that lets classical Nat facts re-enter the δ calculus. Downstream, PeriodExistence uses it to prove Euler's theorem in the residue layer (eulerPeriod_returns_one rewrites periodExponent through toNat_ofNat) and to show the Euler exponent is nonzero. PrimeCoordinateTransform applies it to transfer Nat.Prime p into primeOrbit (ofNat p) and to recover prime power values. SignedOrbitOrderChoiceFree and IntegerRational collapse nonnegativity and integer round-trips to pure Nat inequalities via the same bridge.
In the Recognition stack this sits under the primitive recognition calculus that feeds factorization and grow/order structure; it is bookkeeping, not a forcing step, but without it the δ-native statements of period gaps and prime coordinates cannot cite Mathlib arithmetic. It closes K4.5 in one direction and is already fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.