PRCCharacterNoMixedPrimeWitnesses_iff_no_same_and_no_distinct_pair
plain-language theorem explainer
For a ratio-orbit character χ, absence of mixed prime-axis witnesses is equivalent to the conjunction of two exclusions: no same-prime mixed pair and no distinct-prime mixed pair. Anyone tracking prime-axis orientation purity for native cost uniqueness will cite this. The proof is a short bidirectional constructor chaining the pair-to-witness and same/distinct split lemmas.
Claim. Let $\chi$ be a map on rational orbits. Then $\chi$ has no mixed prime witnesses (no identity-oriented prime axis coexists with a reciprocal-oriented prime axis) if and only if $\chi$ admits neither a same-prime mixed pair witness nor a distinct-prime mixed pair witness.
background
In the Primitive Recognition Calculus, characters act on RatioOrbit displays (signed numerator over a nonzero distinction denominator). Native prime axes are the orbits of prime distinction naturals; a character may send such an axis to itself (identity orientation) or to its reciprocal (reciprocal orientation).
Mixed prime witnesses mean both orientations appear somewhere among prime axes. That global existential splits into pair form: one identity-oriented prime and one reciprocal-oriented prime, which may share the same prime orbit (self-reciprocal branch conflict) or live on distinct primes.
This module develops uniqueness of the native cost from character data. The no-mixing condition is the purity gate that keeps prime-axis orientation coherent before cost reconstruction and the doubled-trace d'Alembert path.
proof idea
Bidirectional constructor.
Forward: from no mixed witnesses, rule out same-pair and distinct-pair separately. Each pair form injects into mixed pair witnesses (..._of_same, ..._of_distinct), then into mixed witnesses (..._of_pair_witnesses); the outer negation fires.
Reverse: from the two negations, use NoMixedPrimeWitnesses_iff_not_mixed_prime_pair_witnesses and the split MixedPrimePairWitnesses_iff_same_or_distinct. Any mixed-pair witness is same or distinct; either arm contradicts the corresponding half of the hypothesis, so mixed pair witnesses are impossible, hence mixed witnesses are impossible.
why it matters
This is the bookkeeping bridge that turns the global no-mixing predicate into independent same-axis and distinct-axis exclusions. Downstream, PRCCharacterNoMixedPrimeWitnesses_iff_not_distinct_prime_pair collapses further once same-axis mixing is already ruled out, and the universal foundation certificate prc_universal_foundation_conditional_certificate consumes the cleaned character hypotheses.
In the Recognition stack this sits under native cost uniqueness for the PRC character: orientation purity on prime axes is required before the character can be identified with the J-cost / doubled-trace data that feeds the forcing chain (T5 J-uniqueness and the Recognition Composition Law). Without the same/distinct split, later one-sided exclusions would have to re-case on equality of primes ad hoc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.