not_unit_ofNat_of_ne_one

In the Primitive Recognition Calculus, DistinctionNat is the native carrier of finite δ-orbit positions. The map from Lean Nat into that carrier is recursive (zero to the zero orbit, successor to succ), and the round-trip theorem records that transporting out and back is the identity on Nat.

Multiplicative structure on the orbit is developed in OrbitDivisibility. A unit is defined to be equality with the one-step orbit; equivalently, by the characterization lemma, an orbit element is a unit if and only if its Nat image equals 1. The only multiplicative unit in the finite δ-orbit is therefore that one-step position.

This lemma sits between those two facts: it converts a plain Nat inequality $n \neq 1$ into the native statement that the embedded orbit is non-unit.

Assume for contradiction that the embedded orbit is a unit. Rewrite with the unit characterization to obtain that its Nat image equals 1. Rewrite again with the ofNat/toNat identity so the image is exactly $n$. The hypothesis $n \neq 1$ then discharges the goal. Pure rewrite-and-exact; no induction.

The sole downstream consumer is the biconditional that native nontrivial factorization displays as ordinary Nat nontrivial factorization. That theorem needs both factors to be nonzero and non-unit on the orbit side, and the corresponding Nat factors to satisfy $a,b \neq 1$. This lemma supplies the non-unit direction when the factors are built by embedding Nat.

It is local arithmetic scaffolding inside the Primitive Recognition Calculus, not a forcing-chain landmark. It keeps the native divisibility language honest relative to ordinary Nat so later prime-orbit and factorization statements can move freely between the two presentations.