PRCCharacterMixedPrimeWitnesses_of_pair_witnesses
plain-language theorem explainer
A ratio-orbit character that carries a single joint package of mixed-prime witnesses (one prime axis identity-oriented, another reciprocal-oriented) also carries the split conjunction form of those witnesses. Native-cost uniqueness arguments that track the mixed-prime obstruction cite this bridge. The proof is a pure unpacking of one joint existential into two separate existentials.
Claim. Let $\chi$ be a map on ratio orbits. If there exist native primes $p$ and $r$ such that $\chi$ is cross-equal to the identity on the prime direction of $p$ and cross-equal to the reciprocal on the prime direction of $r$, then $\chi$ admits both an identity-oriented prime witness and a reciprocal-oriented prime witness (possibly on different primes).
background
In the primitive recognition calculus, ratio orbits are rational displays: a signed numerator orbit over a nonzero distinction-nat denominator. Characters here are maps $\chi$ on those orbits. Native primes supply distinguished axes via prime directions.
The mixed-prime obstruction records that $\chi$ is identity-oriented on some prime axis and reciprocal-oriented on some (possibly different) prime axis. The split form is a conjunction of two existentials; the pair form packages both branches inside one joint existential, removing a propositional wrapper around the obstruction.
Cross-equality is the native equality relation on ratio orbits used to state orientation (identity versus reciprocal) without leaving the discrete orbit language.
proof idea
Term-mode unpacking only. Destructure the pair-packaged hypothesis into primes $p,r$ with their primality proofs and the two cross-equality facts. Rebuild the split conjunction by packaging $(p,$ identity orientation$)$ as the first existential and $(r,$ reciprocal orientation$)$ as the second. No arithmetic or orbit lemmas are invoked.
why it matters
This is one direction of the equivalence between split and pair-packaged mixed-prime witness forms, and it is the half used when a joint package must be reopened as a conjunction. Downstream it feeds the several "no mixed-prime witnesses" characterizations (negation of the pair form, and the same-versus-distinct prime pair splits), the lift from pair-witness characters to prime-calibrated mixed-prime witness characters, and ultimately the conditional universal-foundation certificate in the PRC stack.
In the Recognition forcing picture this sits inside native cost uniqueness for characters: mixed identity/reciprocal prime orientations are the discrete obstruction that must be ruled out (or calibrated) before the native cost is forced toward the unique $J$-shape from the T5 step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.