orbitPositionTrace_comparable
plain-language theorem explainer
Any two native orbit-position traces are comparable under finite extension: one is a prefix of the other. Native-cost uniqueness arguments for ratio characters cite this to transport prime-axis identities without choosing a preferred length. The proof cases on verifier lengths and applies the monotone orbit-trace extension lemma.
Claim. For any two finite distinction-orbit positions $p$ and $r$, either the native orbit trace of $p$ is extended by that of $r$, or the native orbit trace of $r$ is extended by that of $p$.
background
In the Primitive Recognition Calculus a finite trace is empty or built by successive distinction acts. Extension means the longer trace is the shorter one followed by some suffix. Distinction-orbit positions are the base-neutral finite orbits of repeated distinction; their verifier map reads off the iteration count as an ordinary natural number.
The native orbit-position trace is defined by recursion on that $\delta$-orbit rather than by importing verifier naturals into the object theory: the zero position carries the empty trace, and each successor appends one step. Consequently every such trace is a pure initial segment of the infinite step chain, ordered by length.
The surrounding module develops uniqueness of the native cost attached to ratio characters. Comparability of these traces is the elementary lattice fact that any two prime-axis positions already admit a common finite $\delta$-extension.
proof idea
Case on the verifier inequality $p.\mathrm{toNat}\le r.\mathrm{toNat}$. On the true branch, apply the already-proved monotone lemma that a smaller (or equal) orbit length yields an extending native trace, giving the left disjunct. On the false branch, omega recovers the reverse inequality, and the same monotone lemma supplies the right disjunct. No new induction is performed here; the work is total order of lengths plus one upstream extension lemma.
why it matters
This is the comparability engine inside the native-cost uniqueness stack. Parent theorems invoke it directly: prime-identity common-extension respect and prime-identity trace coherence both pass the disjunction as the missing comparable-trace hypothesis; nonunit-identity branch transport and floor-orbit successor transport sit one layer above those. The same fact appears in the dependency cone of the native-cost uniqueness blocker certificate.
In the Recognition Science forcing picture the result is local scaffolding under T5 $J$-uniqueness: once characters respect the totally ordered $\delta$-orbit traces, the native cost functional is forced rather than chosen. Without automatic comparability, common finite extensions would have to be hypothesized at every transport step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.