PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_of_trace_connected
plain-language theorem explainer
If prime calibration forces reciprocal orientation at the orbit-2 prime axis to transport along any finite δ-trace connection to a native prime axis, then once that axis sits on the reciprocal branch every native prime axis does too. Native-cost uniqueness and reciprocal-globalization arguments cite this implication. The proof is a one-line character-level reduction: instantiate the target hypothesis and apply the pointwise trace-connected-to-forces lemma.
Claim. Assume that for every ratio-orbit character $\chi$ that is prime-direction calibrated, reciprocal orientation at the orbit-$2$ prime axis transports along any finite $\delta$-trace connection to a native prime axis. Then, for every such $\chi$, once the orbit-$2$ prime axis lies on the reciprocal branch, every native prime axis lies on the reciprocal branch.
background
In the Primitive Recognition Calculus, ratio-orbit characters encode how recognition orients along multiplicative orbits. Prime-direction calibration fixes preferred orientation at distinguished prime axes. The orbit-$2$ prime axis is the distinguished axis for the reciprocal branch: reciprocal means the character flips orientation relative to the identity branch.
Two target propositions package globalization of that reciprocal choice. The trace-connected target asks that reciprocal orientation at orbit $2$ transport along any finite $\delta$-trace path to an arbitrary native prime axis. The forces target asks the coarser conclusion that every native prime axis is reciprocal once orbit $2$ is. Upstream, the character-level lemma already shows that respecting trace-connected reciprocal transport implies the forces statement for a fixed character: it simply specializes the transport hypothesis at each native prime.
proof idea
One-line wrapper at the target (Prop) level. Introduce a character $\chi$ with the ratio-character and prime-calibration hypotheses. Instantiate the assumed trace-connected target at $\chi$ to obtain the character-level property that two-prime reciprocal respects finite $\delta$-trace connections. Feed that into the upstream lemma that converts character-level trace-connected reciprocal transport into the forces-all-native-primes statement (itself a trivial specialization of transport at each prime).
why it matters
Supplies one direction of the equivalence between the two reciprocal globalization targets (paired with the converse in the local iff theorem). Downstream it is wired into the native-cost uniqueness blocker certificate and into the conditional universal-foundation certificate. Inside Recognition Science this sits in the native $J$-cost uniqueness program (forcing-chain T5): reciprocal branch selection must globalize from orbit-$2$ calibration so the cost character is forced. A sibling identity-branch transport theorem also consumes the reciprocal form via reciprocal twist, so the implication keeps both branches of the split globalization target aligned.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.