PRCCharacterMixedPrimePairWitnesses_iff_same_or_distinct
plain-language theorem explainer
A ratio-orbit character admits a mixed-prime pair witness exactly when it admits either a same-axis or a distinct-axis mixed-prime pair witness. Anyone discharging the mixed-prime obstruction for native cost uniqueness cites this classical split. The proof is a one-line Iff packaging of the two directed lemmas already proved in-module.
Claim. For any map $\chi$ from ratio orbits to ratio orbits, $\chi$ has a mixed-prime pair witness (some prime axes $p,r$ with $\chi$ identity-oriented on $p$ and reciprocal-oriented on $r$) if and only if it has a same-prime mixed-pair witness or a distinct-prime mixed-pair witness.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed numerator over a nonzero distinction-nat denominator. Characters here are maps $\chi$ on ratio orbits. Native primes supply distinguished axes via primeDirection; RatioOrbit.crossEq is the equality test used to say that $\chi$ fixes an axis or sends it to its reciprocal.
The mixed-prime obstruction is packaged three ways. The pair form asserts existence of (not necessarily distinct) prime orbits $p,r$ with $\chi$ identity-oriented on $p$ and reciprocal-oriented on $r$. The same-axis form adds $p=r$ (self-reciprocal branch conflict). The distinct-axis form adds $p\neq r$. This module sits in the native-cost uniqueness development that forces the J-cost character against prime-axis witnesses.
proof idea
Term-mode Iff constructor. The forward arrow is PRCCharacterMixedPrimePairWitnesses_same_or_distinct (case-split the pair existential on whether the two prime carriers are equal). The reverse arrow is PRCCharacterMixedPrimePairWitnesses_of_same_or_distinct (drop the equality/disequality conjunct from either disjunct). No new arithmetic; pure packaging of the two directed lemmas.
why it matters
Closes the last propositional wrapper around the mixed-prime obstruction so downstream results can reason by cases on same-axis versus distinct-axis conflict. Immediately feeds PRCCharacterNoMixedPrimeWitnesses_iff_no_same_and_no_distinct_pair, which rewrites absence of mixed-prime witnesses as the conjunction of the two negated branches. That hygiene is consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation, part of the certificate stack that promotes PRC kernel, ordered-field, and trace-logic facts toward a universal foundation. In the broader RS chain this is scaffolding for T5 J-uniqueness: ruling out mixed prime-axis characters is how non-J cost candidates are excluded before the RCL forces $J(x)=\cosh(\log x)-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.