PRCCharacterPrimeIdentityRespectsTraceConnected_of_canonical_add_trace
plain-language theorem explainer
If a ratio-orbit character preserves identity orientation under the canonical finite δ-trace merger of two prime axes (the position trace of their sum), then it preserves identity orientation along any finite δ-trace connection between those axes. Native-cost uniqueness arguments cite this to collapse the canonical-add form into the general trace-connected transport rule. The proof is a two-step term composition through the common-trace-extension intermediate.
Claim. Let $\chi$ be a map on rational orbits. If $\chi$ respects prime-identity transport through the canonical add-trace (whenever both prime position traces extend into the position trace of $p+r$, identity orientation on each prime axis is preserved by $\chi$), then $\chi$ respects prime-identity transport along any finite $\delta$-trace connection between prime axes: if two prime axes are trace-connected and $\chi$ fixes the first up to cross-equality, it fixes the second.
background
In the Primitive Recognition Calculus, a rational orbit is an integer numerator over a nonzero distinction-nat denominator. Characters $\chi$ act on these orbits; native cost is recovered from a character via a doubled-trace d'Alembert construction aimed at J-cost uniqueness ($J(x)=(x+x^{-1})/2-1$).
Prime axes are orbits of prime distinction-nats. Identity orientation means $\chi$ fixes a prime direction up to cross-equality. Trace connection means the two prime-axis position traces sit inside some common finite $\delta$-trace extension. The canonical-add form specializes that witness to the position trace of the sum $p+r$, so the only content left is respect for that canonical merger.
Upstream, canonical-add already implies the common-trace-extension form (specialize the arbitrary extension to $p+r$), and common-trace-extension implies the existential trace-connected form (unpack the connecting witness). This theorem packages that ladder into one arrow.
proof idea
Pure term-mode composition of two prior implications. Apply the lemma that canonical-add-trace respect yields common-trace-extension respect: the canonical merger $\mathrm{orbitPositionTrace}(p+r)$ is one particular common extension, so the universal quantifier over extensions is discharged by specialization (and the extra extension hypotheses are ignored). Then apply the lemma that common-trace-extension respect yields trace-connected respect: unpack the existential connecting trace from the connectedness hypothesis and feed it to the common-extension rule. No case splits or new algebra.
why it matters
One direction of the equivalence between canonical-add-trace and trace-connected formulations of prime-identity transport; the matching converse sits beside it, and together they give the bidirectional iff in this module. Downstream, prime-calibration forcing of the trace-transport target is obtained by composing calibration-to-canonical-add with this implication. The native-cost uniqueness blocker certificate also rides this chain: collapsing transport formulations is part of showing zero-calibrated native-cost character factorization is forced and signed-admissible alternatives are refuted. At framework scale this supports the T5 J-uniqueness step inside the PRC native-cost layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.