PRCCharacterPrimeIdentityWitnessExcludesReciprocal_of_no_mixed_prime_orientation
plain-language theorem explainer
If a ratio-orbit character never mixes identity and reciprocal orientations across distinct prime axes, then the existence of any identity-oriented prime witness already forbids every reciprocal-oriented prime witness. Native-cost uniqueness arguments cite this as the atomic one-sided form of prime no-mixing. The proof is a three-line unpack of the existential witness into the universal no-mix hypothesis.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose $\chi$ has no mixed prime orientation: it cannot send one prime direction to itself while sending another prime direction to its reciprocal. Then $\chi$ satisfies one-sided prime witness exclusion: if there exists a prime $p$ with $\chi$ fixing the $p$-direction, then for every prime $r$, $\chi$ cannot send the $r$-direction to its reciprocal.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays (signed numerator over a nonzero distinction-nat denominator). Characters $\chi$ act on these orbits and are later tied to native cost via doubled-trace and d'Alembert structure.
Prime directions are the axes generated by prime distinction-nats. Orientation on such an axis is read by cross-equality: $\chi$ may fix a prime direction (identity orientation) or send it to its reciprocal. Mixed orientation means identity on one prime axis and reciprocal on another; the no-mix predicate rules that out universally over pairs of primes.
The one-sided witness form is weaker-looking but equivalent in spirit: an existential identity witness on some prime already excludes reciprocal orientation on every prime. This module packages those coherence conditions as steps toward uniqueness of the native cost character.
proof idea
Term-mode unpacking, not a deep argument. Introduce the existential identity witness $\langle p, hp, hpId\rangle$ and an arbitrary reciprocal candidate $r$ with hypotheses $hr$, $hrRec$. Feed $p$, $hp$, $r$, $hr$, the identity cross-equality, and the reciprocal cross-equality straight into the no-mixed-prime-orientation hypothesis, which returns False. That is exactly the body of the one-sided exclusion predicate.
why it matters
This is one half of the equivalence between universal prime no-mixing and atomic identity-witness exclusion. The converse direction plus this lemma yield the iff used as a clean rewrite in the native-cost uniqueness stack.
Downstream, the prime-calibration forcing target applies this lemma to push no-mix hypotheses into the witness-exclusion target. The uniqueness blocker certificate ultimately rests on that coherence chain: characters that could invert primes independently would spoil the forced native cost (the J-cost uniqueness line in the forcing chain, T5, and the Recognition Composition Law).
Without collapsing mixed orientation, prime-axis inversions would remain free parameters and native cost would not be unique.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.