PRCCharacterMixedPrimePairWitnesses_of_distinct
plain-language theorem explainer
A ratio-orbit character with distinct-axis mixed-prime pair witnesses automatically has the weaker pair-packaged mixed-prime witness form. Native-cost uniqueness arguments that split same-axis versus distinct-axis obstructions cite this forgetful step. The proof is a three-line existential projection that drops the inequality between the two prime axes.
Claim. Let $\chi$ map ratio orbits to ratio orbits. If there exist native primes $p \neq r$ such that $\chi$ fixes the prime direction of $p$ under cross-equality and sends the prime direction of $r$ to its reciprocal under cross-equality, then the same data (without requiring $p \neq r$) witnesses that $\chi$ has a mixed-prime pair: identity orientation on some prime axis and reciprocal orientation on some prime axis.
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 those orbits. Native prime orbits supply distinguished axes via primeDirection.
Two witness packages record mixed orientation on prime axes. The pair-packaged form asserts existence of primes $p,r$ such that $\chi$ is identity-oriented on $p$'s direction and reciprocal-oriented on $r$'s direction (cross-equality). The distinct-axis strengthening adds $p \neq r$. The same-axis sibling forces both orientations onto one prime.
This module develops uniqueness of the native cost functional for such characters. Mixed-prime witnesses are the residual obstruction being classified and eventually excluded under calibration hypotheses.
proof idea
Term-mode existential forgetful map. Unpack the distinct-axis witness as $\langle p, hp, r, hr, _, hpId, hrRec\rangle$, discarding the $p \neq r$ conjunct, and repackage $\langle p, hp, r, hr, hpId, hrRec\rangle$ as a mixed-prime pair witness. No lemmas beyond the two Prop definitions are required.
why it matters
Closes the distinct branch of the same-or-distinct case split: PRCCharacterMixedPrimePairWitnesses_of_same_or_distinct applies this on the right disjunct. It also feeds the two iff characterizations of having no mixed-prime witnesses (versus no same-axis and no distinct-axis packages, and versus not having a distinct prime pair). Downstream, the prime-calibrated lift PRCPrimeCalibratedMixedPrimePairWitnessCharacter_of_distinct reuses the same forgetful step on calibrated characters.
In the Recognition forcing chain this sits inside native cost uniqueness for the J-cost character (T5 J-uniqueness and the Recognition Composition Law background). It does not itself force $\phi$ or dimension; it only tidies the propositional packaging of the mixed-prime obstruction so later uniqueness theorems can quote a single witness form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.