PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_of_split
plain-language theorem explainer
From the split reciprocal-globalization target (prime-to-two transport conjoined with two-to-all transport under prime calibration), extract the distinguished-axis half: once calibration puts the orbit-2 prime axis on the reciprocal branch, every native prime axis is reciprocal. Cited by the iff that collapses the split onto this branch and by the native-cost uniqueness and universal-foundation certificates. Proof is a one-line second-conjunct projection.
Claim. Assume the split reciprocal-globalization target: prime calibration forces both prime-to-two reciprocal transport and two-to-all reciprocal transport. Then the distinguished-axis branch holds: for every ratio-orbit map $\chi$ that is a PRC ratio character and is prime-direction calibrated, if 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, cost uniqueness is tracked through ratio-orbit characters $\chi$ and how prime calibration orients them. A character is prime-direction calibrated when its action on prime axes matches a fixed orientation convention. Reciprocal branch membership means the character sends the axis to its reciprocal rather than the identity orientation.
The module packages reciprocal globalization as a split target: the conjunction of (i) arbitrary-prime-to-orbit-2 reciprocal transport and (ii) orbit-2-to-all-primes reciprocal transport, both forced by prime calibration. The second conjunct is the distinguished-axis target: once the orbit-$2$ axis is reciprocal, every native prime axis is reciprocal.
Upstream, that split is only a named Prop (a conjunction of the two branch targets). This theorem is the right-projection arrow out of that conjunction.
proof idea
One-line wrapper. The hypothesis is definitionally a conjunction whose second factor is exactly the desired target Prop. The proof applies the second projection (.2) and stops. No character unfolding, no calibration lemmas, no d'Alembert or trace identities are invoked.
why it matters
Closes the right half of the split packaging used to organize reciprocal globalization under prime calibration. Downstream, the sibling iff theorem equates the full split target with this distinguished-axis target alone (pairing this projection with the converse packaging arrow). That collapsed form feeds prc_native_cost_uniqueness_blocker_certificate, which records which factorization and signed-admissible targets are proved or refuted on the path to native cost uniqueness.
It also appears in the universal-foundation conditional certificate chain, where PRC kernel, real-complete ordered field, and trace-logic pieces are assembled. In the broader RS forcing picture this is bookkeeping on the J-cost uniqueness side (T5): characters must sit on the reciprocal branch consistently across prime axes before the native cost can be identified with the unique J satisfying the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.