PRCCharacterPrimeIdentityTraceCoherent_of_common_trace_extension
plain-language theorem explainer
If a ratio-orbit character transports prime identity orientation whenever two prime axes sit in one common finite δ-trace, then identity at any calibrated prime forces identity at every calibrated prime. Native-cost uniqueness and the prime-calibration forcing targets cite this implication. The proof instantiates the common extension as the orbit-position trace of the sum of the two primes and applies the left/right extension lemmas.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that whenever two prime axes $p$ and $r$ both extend into a common finite $\delta$-trace $T$, identity orientation of $\chi$ on $p$ forces identity orientation of $\chi$ on $r$. Then identity orientation of $\chi$ at any calibrated prime forces identity orientation at every calibrated prime.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays (signed numerator over a nonzero distinction-nat denominator). A character $\chi$ assigns to each ratio orbit another ratio orbit; identity orientation on a prime axis means $\chi$ fixes that prime direction up to the native cross-equality relation.
Prime identity trace coherence is the missing cross-prime law: the ordinary ratio-character axioms are local to multiplication and reciprocal and do not connect orientation choices on distinct prime axes. The stronger common-trace-extension form says the same transport holds whenever both prime-axis traces embed in one finite $\delta$-trace $T$.
Native orbit-position traces are built by recursion on the $\delta$-orbit (orbitPositionTrace), not by importing verifier naturals. The sum $p+r$ therefore supplies a concrete common extension: both orbitPositionTrace p and orbitPositionTrace r extend into orbitPositionTrace (p+r).
proof idea
Term-mode specialization of the hypothesis. Fix primes $p,r$ and an identity-orientation hypothesis at $p$. Instantiate the common-trace witness as $T := \mathrm{orbitPositionTrace}(p+r)$. Discharge the two extension premises by orbitPositionTrace_add_extends_left and orbitPositionTrace_add_extends_right, then apply the common-trace-extension hypothesis to conclude identity orientation at $r$. No further algebraic work.
why it matters
Closes one direction of the equivalence between the explicit common-trace-extension transport rule and bare prime-identity trace coherence, used immediately by PRCCharacterPrimeIdentityRespectsCommonTraceExtension_iff_trace_coherence. Downstream, prime-calibration forcing targets reduce to this implication (PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_of_common_trace_extension), and the native-cost uniqueness blocker certificate packages the resulting coherence into the uniqueness ledger.
In the Recognition foundation this is bookkeeping for J-cost uniqueness on the native character side: without cross-prime identity transport, local character laws cannot force a single global cost. It sits under the PRC native-cost uniqueness program that feeds the forcing chain toward T5 (J-uniqueness) rather than stating T5 itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.