orbitPositionTrace_add_extends_left
plain-language theorem explainer
Adding any distinction-count r on the right lengthens the orbit-position trace of p: the shorter trace is a prefix of the longer one. Used throughout PRC native-cost uniqueness to connect prime-axis traces and character identities along additive extensions. Proved by induction on r, using reflexivity at zero and one-step extension in the successor case.
Claim. For any distinction naturals $p$ and $r$, the orbit-position trace of $p$ extends to the orbit-position trace of $p+r$: there exists a suffix trace $V$ such that appending $V$ to the orbit-position trace of $p$ recovers the orbit-position trace of $p+r$.
background
In the Primitive Recognition Calculus, a Trace is a finite word in distinction acts (empty or one-step extended). Extension means the longer trace is the shorter one followed by some suffix: $\mathrm{Extends}(T,U)$ iff $\exists V,, T{+}{+}V = U$. Reflexivity holds via the empty suffix.
DistinctionNat is the base-neutral inductive count of repeated distinction (zero / successor), the finite orbit length type. Addition on it is the usual Peano sum; the module supplies add_zero_eq and add_succ_eq. The orbit-position trace of a count is the canonical Trace that records walking that many steps along the orbit.
This lemma lives in the native-cost uniqueness development: characters and doubled-trace costs must respect common trace extensions along the prime axis, so additive lengthening of orbit-position traces is the basic geometric fact.
proof idea
Induction on $r$.
Zero case: $p+0=p$ by add_zero_eq, so the two traces coincide; apply extends_refl.
Successor case: rewrite $p+\mathrm{succ},r = \mathrm{succ}(p+r)$ via add_succ_eq. The inductive hypothesis gives a suffix $V$ with append equal to the orbit-position trace of $p+r$. Take one further step of that suffix (Trace.step), and simplify using the definition of orbit-position trace and the IH equality to match the orbit-position trace of $p+\mathrm{succ},r$.
why it matters
Feeds the right-add twin immediately (commute then apply this lemma), and the comparison form: whenever $p.\mathrm{toNat}\le r.\mathrm{toNat}$, the orbit-position trace of $p$ extends to that of $r$ by writing $r=p+k$.
Those extension facts discharge PRCPrimeAxisTraceConnected_proved: any two prime-orbit counts share the common extension given by the orbit-position trace of their sum. Downstream, canonical-add-trace hypotheses on ratio characters imply branch uniformity, common-trace-extension respect, and trace coherence for prime-identity characters. That chain is part of locking the native cost (J-type) uniqueness in the PRC foundation, upstream of the forcing landmarks that pin $J$ and $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.