PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget_of_common_trace_extension
plain-language theorem explainer
If prime calibration forces identity orientation to respect common finite δ-trace extensions, then it also forces identity orientation invariant along native prime-axis trace connections. Native-cost uniqueness arguments cite this as the reduction from the sharper common-extension target to the weaker transport target. The proof is a one-line wrapper applying the character-level common-extension-to-connected implication.
Claim. Assume that for every ratio character $\chi$ that is prime-direction calibrated, identity orientation respects an explicitly witnessed common finite $\delta$-trace extension. Then for every such $\chi$, identity orientation is invariant along native prime-axis trace connections.
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 restricts how $\chi$ behaves on the prime axis. Two nested targets package what calibration should force for identity orientation.
The weaker target asks only that identity orientation be invariant along native prime-axis trace connections (the connectivity of that graph is already established). The sharper target requires identity orientation to respect an explicitly witnessed common finite $\delta$-trace extension. The character-level lemma already shows that common-extension respect implies trace-connected respect for a fixed $\chi$.
This declaration lifts that implication from a single character to the universal calibration targets: the common-extension target implies the transport target.
proof idea
One-line wrapper. Introduce a ratio character $\chi$ with the ratio-character and prime-direction-calibration hypotheses. Instantiate the common-extension target hypothesis at $\chi$ to obtain common-extension respect, then apply the character-level theorem that common-extension respect implies trace-connected respect. No extra algebraic work.
why it matters
Closes the gap between the sharper common finite $\delta$-trace extension target and the smaller prime-axis trace-transport target inside native-cost uniqueness. Downstream, the propagation theorem that rebuilds the full prime-calibration propagation target from sharpened orientation uses this reduction, and the native-cost uniqueness blocker certificate sits on the same uniqueness spine. In the Recognition forcing chain this is bookkeeping on the cost side (J-uniqueness / T5 and the Recognition Composition Law), not a new physical constant: it ensures prime-calibrated identity orientation transports cleanly along the prime-axis trace graph before uniqueness is certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.