PRCCharacterPrimeIdentityRespectsCanonicalAddTrace_of_common_trace_extension
plain-language theorem explainer
If a ratio-orbit character transports identity orientation whenever two prime axes share any common finite δ-trace extension, then it transports identity through the canonical merger given by the position trace of p+r. Anyone equating the two formulations of prime-identity transport cites this direction. The proof is a one-line specialization of the common-extension hypothesis to that canonical add-trace.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that whenever two prime axes $p,r$ have position traces both extending a common finite $\delta$-trace $T$, identity orientation under $\chi$ on $p$ forces identity orientation on $r$. Then the same transport holds when $T$ is specialized to the canonical add-trace: the position trace of $p+r$.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays (signed numerator over a nonzero distinction-nat denominator). Characters $\chi$ act on these orbits; prime directions are the axes associated to prime orbit positions. Identity orientation means $\chi$ fixes a prime direction up to the cross-equality relation on ratio orbits.
Traces are native $\delta$-histories built by recursion on distinction-nats: the position trace of $n$ is the empty trace at zero and a single step extension at successors. Extension is the prefix order on traces. The common-trace form of prime-identity transport quantifies over an arbitrary finite common extension $T$ of the two prime position traces. The canonical-add-trace form drops that witness and uses only the specific merger $\mathrm{orbitPositionTrace}(p+r)$.
This module develops native-cost uniqueness for PRC characters. The two transport props are intermediate calibration hypotheses: they say identity on one prime axis forces identity on another once the axes sit inside a shared finite $\delta$-trace.
proof idea
One-line specialization. Unfold the target (canonical-add-trace transport), introduce the two primes, the two extension hypotheses for $\mathrm{orbitPositionTrace}(p+r)$, and the identity hypothesis on $p$. Apply the common-trace hypothesis with witness $T := \mathrm{orbitPositionTrace}(p+r)$; the remaining hypotheses match exactly.
why it matters
This is one half of the equivalence between common-trace and canonical-add-trace prime-identity transport. The parent iff packages both directions so later calibration work can switch formulations freely.
Downstream, prime-calibration targets that force identity transport are rewritten from the common-extension shape into the canonical-add-trace shape by applying this lemma. That rewrite feeds the native-cost uniqueness blocker certificate, which records which factorization targets are proved and which signed-admissible variants are refuted.
In the broader forcing picture this sits under native J-cost uniqueness for PRC characters (the T5/RCL lineage): characters that respect prime identity along canonical finite mergers are the ones eligible for cost reconstruction. The lemma itself is pure transport bookkeeping; the physics content lives in the calibration hypotheses it rearranges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.