orbitPositionTrace_extends_of_toNat_le
plain-language theorem explainer
If two orbit positions satisfy p ≤ r in natural value, the finite distinction trace of p is a prefix of the trace of r. Comparability and native-cost uniqueness arguments cite this monotonicity fact. The proof builds the difference orbit k, recovers r = p + k by toNat injectivity, and applies left-extension under addition.
Claim. Let $p,r$ be finite distinction-orbit positions. If the natural iteration count of $p$ is at most that of $r$, then the orbit-position trace of $p$ extends to the orbit-position trace of $r$: there exists a suffix trace $V$ with $\mathrm{append}(T_p,V)=T_r$.
background
In Primitive Recognition Calculus, a Trace is a finite sequence of distinction acts (empty or one-step extension). Extension means the second trace is the first followed by some suffix: $\mathrm{Extends}(T,U)$ iff $\exists V,,\mathrm{append}(T,V)=U$.
DistinctionNat is the base-neutral finite orbit of repeated distinction (zero/successor), the PRC stand-in for $\mathbb{N}$. The map toNat reads off the iteration count; ofNat rebuilds an orbit from a verifier natural. Addition on orbits is recovered under toNat (toNat_add), so arithmetic inequalities on counts translate to orbit equations.
The local module develops native-cost uniqueness for PRC: characters, doubled traces, and d'Alembert-type identities that force the J-cost shape. Orbit-position traces are the concrete finite witnesses whose prefix order must be total before cost comparison can be unique.
proof idea
Set $k:=\mathrm{ofNat}(r.\mathrm{toNat}-p.\mathrm{toNat})$. Prove $p+k=r$ by injectivity of toNat: rewrite with toNat_add and toNat_ofNat, then close the Nat identity by omega. Rewrite the goal along $r=p+k$ and finish with the already-proved left-extension lemma: the orbit-position trace of $p$ extends to that of $p+k$.
why it matters
Immediate parent is orbitPositionTrace_comparable, which cases on $p.\mathrm{toNat}\le r.\mathrm{toNat}$ and invokes this lemma (or the symmetric case) to get total prefix order on orbit-position traces. That comparability feeds the native-cost uniqueness blocker certificate in the same module, part of the PRC path that pins the cost functional to the unique J-shape forced later in the T5/RCL chain.
Without monotone extension of orbit traces under the natural order, doubled-trace and character-matching arguments cannot align costs along a common refinement. The lemma is small bookkeeping, but it is the order-theoretic hinge between discrete orbit arithmetic and trace geometry in the uniqueness pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.