PRCCharacterPrimeIdentityWitnessExcludesReciprocal_iff_no_mixed_prime_orientation
plain-language theorem explainer
On a ratio-orbit character, one-sided prime-axis witness exclusion (any identity-oriented native prime witness forbids every reciprocal-oriented prime witness) is equivalent to global no-mixed prime orientation. Native-cost uniqueness and universal-foundation certificate authors cite this bridge when swapping local witnesses for the universal coherence form. The proof is a two-constructor Iff term applying the two one-direction lemmas.
Claim. For any map $\chi$ from ratio orbits to ratio orbits, the following are equivalent: (i) if there exists a prime distinction-natural $p$ such that $\chi$ fixes the prime direction of $p$ up to cross-equality, then $\chi$ never sends any prime direction to its reciprocal; (ii) $\chi$ cannot fix one prime direction while sending another prime direction to its reciprocal.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer-numerator display over a nonzero distinction-natural denominator. Characters $\chi$ act on these orbits; the native-cost uniqueness development studies which characters are compatible with the cost/trace calculus.
Prime directions are the axes attached to prime distinction-naturals. A character may orient such an axis by identity (cross-equality with the prime direction) or by reciprocal (cross-equality with the reciprocal orbit). No-mixed prime orientation forbids identity on one prime axis together with reciprocal on another: it is the trace-coherence condition that rules out independent prime-axis inversions.
The witness form is the atomic one-sided version: once any identity-oriented native prime witness exists, no reciprocal-oriented native prime witness can coexist with it. The two one-direction lemmas already convert between these presentations; the present declaration packages them as a single equivalence.
proof idea
Term-mode $\leftrightarrow$ introduction. The left-to-right arm is the lemma that turns identity-witness exclusion into no-mixed orientation: given primes $p,r$ with identity on $p$ and reciprocal on $r$, package $\langle p,\mathrm{id}\rangle$ as the existential witness and apply exclusion. The right-to-left arm is the converse lemma: unpack the existential identity witness and feed it with the reciprocal witness into the universal no-mixing quantifiers. Both arms are pure quantifier rewrites; no arithmetic or orbit algebra is invoked.
why it matters
The equivalence lets the uniqueness pipeline treat the atomic witness form and the global coherence form interchangeably, so later certificates need not fix one presentation. Downstream it is used by the native-cost uniqueness blocker certificate and by the conditional universal-foundation certificate.
In the Recognition Science forcing chain, native cost uniqueness underwrites the path to J-uniqueness (T5): characters that mix prime orientations would break the d'Alembert/trace coherence that forces $J(x)=(x+x^{-1})/2-1$. Closing this bookkeeping gap between local witnesses and global orientation constraints removes a presentation mismatch inside that foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.