orbitPositionTrace_add_extends_right
plain-language theorem explainer
The orbit-position trace of a distinction natural r is always a prefix of the orbit-position trace of p+r. Anyone assembling common-trace witnesses on the prime axis, or proving character identities that respect canonical add-traces, cites this. The argument is a one-line reduction: commute addition and apply the left-extension lemma.
Claim. For distinction naturals $p$ and $r$, the orbit-position trace of $r$ extends to the orbit-position trace of $p+r$: there is a suffix trace $V$ such that appending $V$ to the orbit-position trace of $r$ recovers the orbit-position trace of $p+r$.
background
In the Primitive Recognition Calculus, a Trace is a finite sequence of distinction acts (empty, or one act appended). The relation Extends says that one trace is another followed by some suffix: $\mathrm{Extends},T,U$ means $\exists V,,\mathrm{append},T,V=U$. DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor), with its own addition.
The orbit-position trace assigns to each DistinctionNat the canonical Trace that records walking that many steps along the orbit. The left-extension lemma already states that the orbit-position trace of $p$ extends to that of $p+r$. This module develops native cost uniqueness for PRC characters, so both left and right prefix facts are needed to build a common supertrace for a pair of prime-orbit positions.
proof idea
One-line wrapper. Rewrite $p+r$ as $r+p$ by DistinctionNat addition commutativity, then apply the left-extension lemma at arguments $(r,p)$. No separate induction or case split is required.
why it matters
Together with the left-extension lemma, this supplies the two Extends legs of PRCPrimeAxisTraceConnected_proved: the common supertrace is the orbit-position trace of $p+r$, with left and right prefix witnesses. Downstream, that connectedness feeds the character-side infrastructure: PRCCharacterPrimeIdentityRespectsCommonTraceExtension_of_canonical_add_trace, the branch-uniform and trace-coherent variants, and ultimately the native-cost uniqueness path for ratio characters. In the forcing chain this sits under the PRC foundation that pins the unique cost functional (T5 J-uniqueness / RCL) before phi and the eight-tick structure appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.