PRCCharacterMixedPrimePairWitnesses_of_same_or_distinct
plain-language theorem explainer
If a ratio-orbit character carries either a same-axis or a distinct-axis mixed-prime pair witness, then it carries the unordered mixed-prime pair witness. Native-cost uniqueness arguments cite this to collapse the same/distinct case split into one obstruction package. The proof is a two-branch case split that forgets the equality or inequality of the prime axes.
Claim. Let $\chi$ be a map on rational orbits. If either (i) there exist native prime orbits $p=r$ with $\chi$ fixing the identity-oriented prime direction of $p$ and sending the prime direction of $r$ to its reciprocal, or (ii) the same holds for some $p\neq r$, then there exist (not necessarily related) native primes $p,r$ witnessing that mixed pair of cross-equalities.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed numerator over a nonzero distinction-nat denominator. Characters $\chi$ act on these orbits. Native prime directions are the axes along which cost and trace constraints are checked.
A mixed-prime pair witness packages two branch conditions at once: $\chi$ agrees with the identity on one prime direction (cross-equality), and agrees with reciprocal on another. The same-axis form forces both witnesses onto one prime orbit (self-reciprocal branch conflict). The distinct-axis form places them on different primes. The pair-packaged form drops the $p=r$ / $p\neq r$ tag and keeps only the two cross-equalities.
This module develops native-cost uniqueness for PRC characters. The present lemma is the forgetful direction from the tagged disjunction into the untagged package.
proof idea
Term-mode case split on the hypothesis disjunction. On the left (same-axis) branch, apply PRCCharacterMixedPrimePairWitnesses_of_same, which unpacks the existential, discards $p=r$, and repacks the two cross-equalities. On the right (distinct-axis) branch, apply PRCCharacterMixedPrimePairWitnesses_of_distinct, which likewise discards $p\neq r$. No further arithmetic is needed.
why it matters
Feeds the biconditional PRCCharacterMixedPrimePairWitnesses_iff_same_or_distinct, which equates the untagged mixed-prime obstruction with the same-or-distinct split. That equivalence is the last propositional cleanup around the mixed-prime obstruction used when characters are forced toward the native J-cost.
Also appears in the dependency cone of prc_universal_foundation_conditional_certificate in UniversalFoundation, the conditional certificate assembling kernel, real-complete ordered field, and trace-logic pieces. Within the forcing chain this sits under native-cost uniqueness toward T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$), where mixed identity/reciprocal prime witnesses are the obstruction that a genuine cost character must avoid or resolve.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.