PRCCharacterPrimeIdentityRespectsCommonTraceExtension_of_comparable_trace
plain-language theorem explainer
If a ratio character transports identity orientation between prime axes whenever their finite orbit traces are comparable by extension, then it also transports identity when both axes sit in a common finite δ-trace extension. Native-cost uniqueness and prime-calibration force lemmas cite this packaging bridge. The proof is a one-line reduction: any two orbit-position traces are always comparable, so the common-extension data is discharged by that structural fact.
Claim. Let $\chi$ map rational orbits to rational orbits. Suppose that whenever two prime-orbit axes have comparable finite $\delta$-orbit traces (one extends the other) and $\chi$ fixes the first prime direction up to cross-equality, then $\chi$ also fixes the second. Then the same identity transport holds whenever both prime-orbit traces extend into some common finite trace $T$.
background
In the Primitive Recognition Calculus, a ratio orbit packages a signed numerator over a nonzero distinction-natural denominator. Prime directions are the axes of prime orbits. A ratio character $\chi$ acts on these orbits; identity orientation means $\chi$ fixes a prime direction up to cross-equality.
Finite $\delta$-orbit traces record successive positions under the recognition dynamics. Trace extension is the natural continuation order. The module already proves that any two orbit-position traces are comparable: one always extends the other, by comparing underlying natural sizes (orbitPositionTrace_comparable).
Two packagings of the identity-transport law appear. The comparable-trace form requires an extension order between the two prime traces. The common-extension form requires both traces to embed in a shared finite witness $T$. The latter is the explicit shape used by calibration targets downstream.
proof idea
One-line wrapper. Introduce the common-extension data (primes $p,r$, a common trace $T$, extension witnesses, and the identity hypothesis on $p$). Discard $T$ and both extension witnesses. Apply the comparable-trace hypothesis to $p$ and $r$, supplying the structural lemma that orbit-position traces of any two distinction naturals are always comparable by extension. The identity hypothesis on $p$ then yields identity on $r$.
why it matters
This bridges the two packagings of the prime-identity transport law inside native cost uniqueness. Downstream, the trace-coherence route factors through it: coherence implies the comparable-trace law, which this theorem lifts to the common-extension law. The prime-calibration force target likewise reduces its common-extension form to the comparable-trace form via this lemma. Both feed the native-cost uniqueness blocker certificate that records which factorization targets are proved or refuted.
In the Recognition Science forcing chain, native cost uniqueness is the local engine that pins the J-cost (T5: $J(x)=(x+x^{-1})/2-1$) as the unique cost compatible with the Recognition Composition Law on the phi-ladder. This lemma is pure packaging glue, not a physics step, but without it the common-extension targets used by the certificate do not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.