PRCCharacterPrimeIdentityRespectsCommonTraceExtension_of_canonical_add_trace
plain-language theorem explainer
Canonical prime-identity transport for a ratio-orbit character implies the common-trace form: if identity orientation on one prime axis forces the other through the fixed merger orbitPositionTrace(p+r), then the same holds for every finite δ-trace that jointly extends both axes. Cited when collapsing the two formulations of prime-identity transport. Proof is a short term application of the two add-extension lemmas for orbit-position traces.
Claim. Let $\chi$ be a map on rational orbits. If $\chi$ respects prime-identity orientation through the canonical finite merger $\mathrm{orbitPositionTrace}(p+r)$ (i.e., whenever the $p$- and $r$-axis traces extend into that merger, identity on the $p$-prime direction forces identity on the $r$-prime direction), then $\chi$ also respects prime-identity orientation for every common finite $\delta$-trace extension $T$ of the two prime-axis traces.
background
In the Primitive Recognition Calculus, ratio orbits package a signed numerator over a nonzero distinction-nat denominator. Prime axes are the prime orbits of distinction naturals; a character $\chi$ acts on ratio orbits. Identity orientation on a prime axis means $\chi$ is cross-equal to the identity on that prime direction.
Two formulations of prime-identity transport appear. The common-trace form asks that identity on one prime axis force identity on another whenever both axis traces sit inside some shared finite $\delta$-trace $T$. The canonical-add-trace form specializes $T$ to the concrete merger $\mathrm{orbitPositionTrace}(p+r)$, removing the arbitrary witness.
Upstream, $\mathrm{orbitPositionTrace_add_extends_left}$ and $\mathrm{_right}$ show that the $p$- and $r$-axis traces always extend into $\mathrm{orbitPositionTrace}(p+r)$. Those facts make the canonical extension premises free, so the canonical rule is the contentful core of common-trace transport.
proof idea
Term-mode, five lines. Introduce the common-trace data $p,r,T$ and the identity hypothesis on the $p$-axis. Discard $T$ and its extension hypotheses. Apply the canonical hypothesis at $p,r$, supplying the two always-true premises $\mathrm{orbitPositionTrace_add_extends_left},p,r$ and $\mathrm{orbitPositionTrace_add_extends_right},p,r$, then pass through the given identity hypothesis. The conclusion is exactly common-trace transport on the $r$-axis.
why it matters
Closes one direction of the equivalence between canonical-add and common-trace prime-identity transport, used immediately by $\mathrm{PRCCharacterPrimeIdentityRespectsCanonicalAddTrace_iff_common_trace_extension}$. Downstream it feeds $\mathrm{PRCCharacterPrimeIdentityRespectsTraceConnected_of_canonical_add_trace}$ and the calibration target $\mathrm{PRCPrimeCalibrationForcesPrimeIdentityCommonTraceExtensionTarget_of_canonical_add_trace}$, and appears in the native-cost uniqueness blocker certificate.
In the Recognition stack this is bookkeeping inside native $J$-cost uniqueness for PRC characters: identity orientation must travel between prime axes under finite $\delta$-trace mergers before the cost functional can be forced. It sits below the T5 $J$-uniqueness landmark (unique cost $J(x)=(x+x^{-1})/2-1$) by locking the character-side transport rule that uniqueness arguments rely on. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.