PRCCharacterMixedPrimePairWitnesses_same_or_distinct
plain-language theorem explainer
Any character that carries a mixed-prime pair witness (one prime axis fixed by χ, another sent to its reciprocal) falls into exactly one of two branches: the two axes are the same native prime, or they are distinct. Case analysts of the mixed-prime obstruction cite this split. The proof is a one-line case split on equality of the two existential prime witnesses.
Claim. Let $\chi$ be a map on rational orbits. If there exist prime orbits $p$ and $r$ such that $\chi$ fixes the prime direction of $p$ and sends the prime direction of $r$ to its reciprocal, then either $p=r$ (same-axis mixed-prime witness) or $p\neq r$ (distinct-axis mixed-prime witness).
background
In the Primitive Recognition Calculus, ratio orbits package a signed numerator over a nonzero distinction-nat denominator. Characters $\chi$ act on these orbits. A prime direction is the orbit associated to a native prime distinction-nat.
The mixed-prime pair witness packages two branch conditions in one existential: $\chi$ agrees with the identity on one prime direction and with reciprocity on another. The same-axis form forces those two primes equal (self-reciprocal branch conflict). The distinct-axis form forces them unequal.
This lemma sits in the native-cost uniqueness development, where such witnesses obstruct characters that would otherwise match the native $J$-cost on the phi-ladder of ratio orbits.
proof idea
Unpack the mixed-prime pair witness to obtain primes $p,r$ with the identity and reciprocal cross-equality conditions. Case on $p=r$. If equal, package the data into the same-axis witness; if unequal, package into the distinct-axis witness. No further lemmas are required beyond the three witness definitions.
why it matters
Gives the forward half of the biconditional equating the packaged mixed-prime witness with the disjunction of same-axis and distinct-axis forms. Downstream, the prime-calibrated mixed-pair character theorem cases on this split, and the universal-foundation conditional certificate pulls the uniqueness stack that depends on clearing these obstructions.
In the Recognition forcing chain, native cost uniqueness feeds the identification of $J$ (T5) as the unique cost compatible with the Recognition Composition Law. Separating self-reciprocal from two-prime conflicts keeps the obstruction analysis modular before calibration to primes and passage to the universal foundation certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.