PRCCharacterNoMixedPrimeWitnesses_of_no_mixed_prime_orientation
plain-language theorem explainer
If a ratio-orbit character never mixes identity orientation on one prime axis with reciprocal orientation on another (universal form), then no pair of mixed prime witnesses can exist (existential form). Used when calibrating native cost uniqueness and when equating the two no-mixing formulations. The proof unpacks the two existential witnesses and feeds them to the universal hypothesis.
Claim. Let $\chi$ be a map on rational orbits. If $\chi$ satisfies the universal no-mixed-prime-orientation condition (for every pair of prime axes, identity orientation on one and reciprocal orientation on the other is impossible), then $\chi$ satisfies the existential no-mixed-prime-witnesses condition: there do not exist both an identity-oriented prime witness and a reciprocal-oriented prime witness.
background
In the Primitive Recognition Calculus, ratio orbits package a signed numerator over a nonzero distinction-nat denominator. Characters act on these orbits; native cost uniqueness tracks how a character orients prime axes, either as the identity direction or as its reciprocal.
No mixed prime orientation is the trace-coherence condition that rules out independent prime-axis inversions: a character cannot choose identity on one prime axis and reciprocal on another. The universal form quantifies over all prime pairs and concludes falsehood from any such mixed pair of orientations.
The existential form packages the same prohibition as the negation of a conjunction of two existence statements: no identity-oriented prime witness can coexist with a reciprocal-oriented prime witness. Both live in the native-cost uniqueness module and feed the prime-calibration chain that forces coherent orientation of the character.
proof idea
Term-mode unpacking of the existential form. Introduce the forbidden conjunction of witnesses via rintro, destructure the identity-oriented witness to a prime $p$ with orientation data, destructure the reciprocal-oriented witness to a prime $r$ with orientation data, then apply the universal no-mixed-prime-orientation hypothesis at those four data. No auxiliary lemmas are needed beyond the two Prop definitions.
why it matters
This is one direction of the equivalence between the universal and existential formulations of prime-axis no-mixing. Downstream, PRCCharacterNoMixedPrimeWitnesses_iff_no_mixed_prime_orientation packages both directions as an iff, so either form may be used in native-cost arguments.
It also lifts calibration targets: PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_of_no_mixed_prime_orientation converts a calibration hypothesis stated in universal orientation language into the existential-witness target used later in the uniqueness pipeline. In the Recognition forcing chain this sits under native J-cost uniqueness (T5 landmark territory): coherent prime orientation is part of forcing the character that yields $J(x)=(x+x^{-1})/2-1$ rather than a mixed-inversion impostor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.