PRCCharacterNoMixedPrimeWitnesses
plain-language theorem explainer
Existential no-mixing condition on a ratio-orbit character: identity-oriented and reciprocal-oriented prime witnesses cannot coexist. Native-cost uniqueness cites it to equate several coherent-orientation formulations. Pure definitional Prop (negation of a mixed-witness pair), no proof content.
Claim. For a map $\chi$ on ratio orbits, it is not the case that there exist primes $p$ and $r$ in the distinction naturals such that $\chi$ is identity-oriented on the prime direction of $p$ and reciprocal-oriented on the prime direction of $r$, with orientation witnessed by cross-multiplication equality of ratio orbits (including against the orbit reciprocal).
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display built from a signed numerator orbit over a nonzero distinction-natural denominator. Cross-multiplication equality is the internal PRC relation that matches rational equality of verifier displays: two orbits agree when scaled numerators balance. The total reciprocal on ratio orbits sends zero to zero and otherwise inverts, mirroring $\mathbb{Q}$.
A character here is a map $\chi$ on ratio orbits. On each native prime axis (the prime direction of a prime distinction natural), $\chi$ may land identity-oriented (cross-equal to the prime direction itself) or reciprocal-oriented (cross-equal to the reciprocal of that direction). Identity orientation sits at the J-cost minimum; reciprocal orientation is the inverse-ratio event from ledger forcing.
This module develops uniqueness of the native cost from character hypotheses. The present predicate is the existential packaging of prime-axis no-mixing used throughout those uniqueness arguments.
proof idea
Definitional Prop only: the body is the negation of a conjunction of two existentials. The first asserts some prime distinction natural whose prime direction is fixed by $\chi$ up to cross-equality; the second asserts some (possibly different) prime whose prime direction is sent by $\chi$ to its orbit reciprocal up to cross-equality. No tactics or lemmas are applied.
why it matters
This is the working form of prime-axis no-mixing in the native-cost uniqueness development. Downstream it is shown equivalent to no mixed prime orientation, to the identity-witness-excludes-reciprocal form, to the negation of mixed prime-pair witnesses, and to the split into same-prime versus distinct-prime mixed pairs. Coherent prime orientation implies it, and it implies the orientation form used when matching doubled-trace native cost to the J-cost character.
In the broader Recognition forcing picture this supports uniqueness of the native cost functional along the path toward T5 J-uniqueness ($J(x)=\cosh(\log x)-1$) and the Recognition Composition Law. It does not itself force $J$; it only rules out characters that mix identity and reciprocal orientations on prime axes, a necessary coherence condition before cost-from-character uniqueness can close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.