PRCCharacterPrimeIdentityRespectsCommonTraceExtension
plain-language theorem explainer
Defines the common-trace transport property for a ratio-orbit character: if two prime axes sit inside one finite δ-trace extension and the character is identity-oriented on the first, it is identity-oriented on the second. Cited when equating canonical-add-trace, comparable-trace, and full trace-coherence forms of prime-identity respect. Pure Prop packaging; no proof content.
Claim. A map $\chi$ on ratio orbits respects common-trace prime-identity transport when: for any two prime distinction-naturals $p,r$, if some finite trace $T$ extends both orbit-position traces of $p$ and $r$, and $\chi$ is cross-equal to the identity orientation on the prime direction of $p$, then $\chi$ is likewise cross-equal to the identity orientation on the prime direction of $r$.
background
In the Primitive Recognition Calculus, a finite trace is built by successive distinction acts (empty, or extend by one act). Trace extension means one trace is a prefix of another: $U$ extends $T$ when $T$ followed by some suffix equals $U$. Each prime distinction-natural has an orbit-position trace and a prime direction on the ratio-orbit space.
A character $\chi$ is a self-map of ratio orbits. Identity orientation means $\chi$ is cross-equal to the identity direction on that orbit (the character fixes the identity event at the $J$-cost minimum $x=1$). The native-cost uniqueness development needs a precise transport rule: identity orientation on one prime axis should force the same on another when both axes are witnessed inside a shared finite $\delta$-trace.
This definition packages that rule with an explicit common extension witness $T$, rather than a fixed canonical merger. Upstream, Extends and Trace supply the K2.4–K2.5 language used in the body.
proof idea
Definitional Prop, not a proved theorem. The body is a five-quantifier implication: primes $p,r$ with prime-orbit certificates, a common finite trace $T$ extending both orbit-position traces, and cross-equality of $\chi$ to the prime direction on $p$, imply the same cross-equality on $r$. No tactics or lemmas; downstream theorems discharge or equate instances of this predicate.
why it matters
Sits in the PRC native-cost uniqueness chain that forces the recognition cost character. Downstream it is equivalent to the canonical-add-trace form (identity transports through the specific finite merger orbitPositionTrace (p + r)), removing the arbitrary common-extension witness. It is also equivalent to full prime-identity trace coherence, via comparable-trace as an intermediate.
Parent results include the iff with canonical-add-trace respect, the one-direction implications from/to canonical add and comparable trace, and the bridge to PRCCharacterPrimeIdentityTraceCoherent. That coherence layer feeds uniqueness of the native cost built from the character, tying back to T5 $J$-uniqueness and the Recognition Composition Law: only characters that transport identity orientation across shared $\delta$-traces can yield the forced $J$-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.