PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget_of_trace_coherence
plain-language theorem explainer
Prime calibration that forces identity orientation to propagate across all prime axes also forces it to be invariant along native prime-axis trace connections. Anyone closing the native-cost uniqueness or universal-foundation certificates cites this one-way reduction. The proof is a short term application of the pointwise coherence-to-transport lemma under the calibrated character hypotheses.
Claim. If prime calibration forces identity orientation to propagate across prime axes (the trace-coherence target), then it also forces identity orientation to be invariant along native prime-axis trace connections (the trace-transport target). Explicitly: whenever $\chi$ is a ratio character that is prime-direction calibrated, the coherence conclusion for $\chi$ yields the connectedness-respect conclusion for $\chi$.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and encode orientation data used to build native costs. Prime-direction calibration is the hypothesis that $\chi$ is aligned on native prime axes. Two residual targets package what calibration must still force about identity orientation.
The coherence target asks that identity orientation propagate across prime axes: every identity-oriented native prime axis puts all native prime axes on the identity branch. The transport target is the smaller demand that identity orientation be invariant along native prime-axis trace connections; structural connectivity of that prime-axis trace graph is already established upstream.
Pointwise, if a single character is prime-identity trace-coherent, then it respects trace-connectedness: identity on one connected prime axis forces identity on any trace-connected prime axis. That pointwise fact is the bridge used here at the target (forall-character) level.
proof idea
Term-mode, three introductions then one application. Introduce a ratio character $\chi$, the ratio-character hypothesis, and prime-direction calibration. Feed those into the coherence-target hypothesis to obtain prime-identity trace-coherence of $\chi$. Apply the upstream lemma that any such coherent character respects trace-connectedness, which is exactly the transport-target conclusion at $\chi$. No extra algebraic work.
why it matters
This is one half of the equivalence between the remaining trace-coherence target and the smaller trace-transport target; the sibling converse closes the iff used when either packaging is more convenient. Downstream it feeds the native-cost uniqueness blocker certificate and the conditional universal-foundation certificate, both of which track which PRC uniqueness obligations are discharged versus still open.
In the Recognition forcing picture this sits inside native-cost uniqueness for the J-cost lineage (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), before phi-ladder mass and constant normalizations. It does not itself force $J$ or $\phi$; it only reduces one residual orientation-propagation obligation to a connectivity-respect form already supported by the proved prime-axis trace graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.