PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_of_trace_transport
plain-language theorem explainer
If prime calibration forces identity orientation to stay invariant along native prime-axis trace connections, then it forces identity orientation to propagate coherently across all prime axes. Anyone closing the native-cost uniqueness chain cites this reduction. The proof is a short term argument that plugs the already-proved full connectivity of the prime-axis trace graph into the transport hypothesis.
Claim. Assume that every prime-direction-calibrated ratio character has identity orientation invariant along every native prime-axis trace connection. Then every such calibrated character has identity orientation that propagates coherently across all prime axes.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits obeying the multiplicative character laws used to rebuild the native cost. Prime-direction calibration means $\chi$ is pinned on the identity branch along each native prime axis. Two residual targets remain for uniqueness: a transport target (identity orientation is invariant along any witnessed prime-axis trace connection) and a coherence target (identity orientation propagates across all prime axes).
The structural fact already on the shelf is that any two prime orbits are trace-connected: for primes $p,r$ there is an explicit finite $\delta$-trace extension (via the orbit-position trace of $p+r$) linking their axes. The transport target is the smaller obligation; coherence is the exact remaining global statement. This lemma records that connectivity turns transport into coherence.
proof idea
Term-mode reduction. Introduce a calibrated character $\chi$ and a pair of prime axes $p,r$ with an identity-orientation hypothesis on one side. Apply the transport hypothesis to $\chi$, the two primes, and the connectivity witness PRCPrimeAxisTraceConnected_proved p hp r hr, then discharge with the given identity pin. No extra algebraic work: connectivity plus transport yields coherence.
why it matters
Closes one direction of the equivalence between the coherence and transport targets, so either form may be used as the residual obligation in the native-cost uniqueness campaign. Downstream, the iff theorem packages both directions, and the sharpened-orientation propagation path consumes the coherence form when lifting local prime orientation to global calibration. The uniqueness blocker certificate ultimately depends on this layer: once prime calibration forces coherent identity orientation, competing signed or non-native factorizations are ruled out. In the broader RS forcing picture this is bookkeeping inside the J-uniqueness / native-cost lane (T5), not a new physical constant, but it is the bridge that lets a local transport lemma finish the global coherence claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.