PRCCharacterPrimeIdentityRespectsCommonTraceExtension_of_trace_coherence
plain-language theorem explainer
Prime-identity trace coherence of a ratio-orbit character implies identity orientation transports across any two prime axes that share a common finite δ-trace extension. Native-cost uniqueness arguments cite this to pass from the global cross-prime coherence hypothesis to the explicit common-extension transport rule. The proof is a two-step term composition through the comparable-trace intermediate.
Claim. Let $\chi$ be a map on rational orbits. If $\chi$ is prime-identity trace-coherent (identity orientation at one calibrated prime forces identity orientation at every calibrated prime), then $\chi$ respects common trace extension: whenever the position traces of two prime axes both extend into the same finite $\delta$-trace $T$, identity orientation of $\chi$ on the first prime axis forces identity orientation on the second.
background
In the Primitive Recognition Calculus, rational data live on ratio orbits: integer numerator over a nonzero orbit denominator. A ratio character $\chi$ acts on these orbits; prime axes are the directions associated to prime distinction-naturals. Identity orientation means $\chi$ fixes a prime direction up to the cross-equality relation on orbits.
Prime-identity trace coherence is the missing cross-prime law: the local multiplicative and reciprocal character axioms do not by themselves link orientation choices on distinct prime axes. Coherence asserts that if any calibrated prime is identity-oriented under $\chi$, then every calibrated prime is.
Common-trace-extension respect is the more explicit transport form used downstream: identity orientation moves between two primes once both of their position traces sit inside one finite $\delta$-trace extension. An intermediate comparable-trace respect property sits between the two formulations.
proof idea
Term-mode composition of two already-proved implications. First apply the lemma that trace coherence yields comparable-trace respect (coherence is strictly stronger than the comparable-trace hypothesis, so the implication is by specializing the universal quantifiers). Then apply the lemma that comparable-trace respect yields common-trace-extension respect, which discharges the shared-extension premises by the fact that any two prime position traces are comparable. No new case analysis appears at this layer.
why it matters
This is one direction of the equivalence between common-trace-extension respect and trace coherence, so the two formulations of the prime-identity transport blocker may be swapped freely. Downstream, the calibration theorem that lifts a prime-calibration-forces-coherence target to a common-trace-extension target is exactly this implication applied under the calibration hypotheses. The native-cost uniqueness blocker certificate also depends on the resulting transport package. In the Recognition forcing chain this sits inside the foundation layer that pins the native cost (the J-cost side of T5) before the self-similar fixed point and eight-tick structure are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.