PRCCharacterNoMixedPrimeWitnesses_iff_not_distinct_prime_pair
plain-language theorem explainer
For a ratio-orbit character χ, the global no-mixed-prime-witness condition is equivalent to the absence of a distinct-prime mixed pair. Same-prime mixed pairs are already absurd, so only distinct axes can produce mixing. Cost-uniqueness and universal-foundation arguments cite this to collapse the no-mixing hypothesis to a single existential negation. The proof is a short bidirectional constructor chaining the mixed-witness hierarchy with the same-prime absurdity lemma.
Claim. Let $\chi$ be a map on rational orbits. Then $\chi$ admits no coexistence of an identity-oriented prime-axis witness with a reciprocal-oriented prime-axis witness if and only if there do not exist distinct native primes $p\neq r$ such that $\chi$ fixes the prime direction of $p$ and sends the prime direction of $r$ to its reciprocal.
background
In the Primitive Recognition Calculus, ratio orbits package signed integer numerators over nonzero distinction denominators. A character $\chi$ acts on these orbits. Prime directions are the native prime axes of the distinction lattice; orientation is read by cross-equality of $\chi$ against the identity direction or its reciprocal.
PRCCharacterNoMixedPrimeWitnesses is the existential no-mixing statement: it is impossible for some prime axis to be identity-oriented while some (possibly other) prime axis is reciprocal-oriented. The distinct-pair form strengthens the positive witness by requiring the two primes to be unequal. The same-prime mixed-pair form is separately known to be absurd.
An intermediate lemma already splits no-mixing into the conjunction of no same-prime mixed pair and no distinct-prime mixed pair. The present result collapses that split once same-prime mixing is ruled out.
proof idea
Bidirectional constructor.
Forward: from no-mixing and a distinct-pair witness, apply PRCCharacterMixedPrimePairWitnesses_of_distinct then PRCCharacterMixedPrimeWitnesses_of_pair_witnesses to obtain a mixed-prime witness, contradicting no-mixing.
Reverse: from absence of a distinct-pair witness, feed PRCCharacterSamePrimeMixedPairWitnesses_absurd together with that absence into the reverse direction of PRCCharacterNoMixedPrimeWitnesses_iff_no_same_and_no_distinct_pair, recovering no-mixing.
why it matters
Native cost uniqueness for PRC characters needs a clean prime-axis no-mixing hypothesis so that the doubled-trace / d'Alembert data force the unique J-cost shape (the T5 landmark $J(x)=(x+x^{-1})/2-1$). This equivalence removes an intermediate same-versus-distinct case split from downstream statements: one may assume only that no distinct-prime mixed pair exists.
It is consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation, which packages kernel, real-complete ordered field, and trace-logic certificates into the conditional universal foundation. Closing the no-mixing side of the character hypotheses is a concrete step toward that certificate's cost-uniqueness branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.