PRCCharacterNoMixedPrimeWitnesses_of_coherent_prime_orientation
plain-language theorem explainer
Coherent prime-axis orientation of a ratio-orbit character forces the existential no-mixing property: identity-oriented and reciprocal-oriented prime witnesses cannot coexist. Anyone calibrating native PRC cost characters on prime directions cites this. The proof is a short case split on the two coherent branches, each reducing mixed witnesses to a prime direction cross-equal to its reciprocal.
Claim. Let $\chi$ be a map on ratio orbits. If prime-axis orientation is coherent for $\chi$ (on every native prime direction, $\chi$ is cross-equal either always to the identity direction or always to the reciprocal direction), then $\chi$ admits no mixed prime witnesses: there cannot exist one native prime axis identity-oriented under $\chi$ and another reciprocal-oriented under $\chi$.
background
In the Primitive Recognition Calculus, ratio data live as RatioOrbit displays (signed numerator over a nonzero distinction-nat denominator). Equality of displays is the internal cross-multiplication relation crossEq (K4.10): two orbits match when scaled numerators balance as signed orbits. Reciprocals are total on this type, sending zero to zero as in $\mathbb{Q}$.
A character $\chi$ acts on ratio orbits. On each native prime direction (the orbit axis attached to a prime distinction-nat), $\chi$ may land on the identity orientation or the reciprocal orientation, witnessed by crossEq. Coherence means a global choice: either every prime direction is identity-oriented, or every one is reciprocal-oriented. No-mixed-prime-witnesses is the existential dual: it is impossible to hold both an identity witness on some prime and a reciprocal witness on some (possibly other) prime.
The local module develops native cost uniqueness for PRC characters; this lemma converts the universal coherence hypothesis into the existential no-mixing form used by calibration targets.
proof idea
Term-mode proof by contradiction on the mixed-witness pair. Unpack an identity witness $(p,h_p)$ and a reciprocal witness $(r,h_r)$. Case-split the coherence hypothesis.
If every prime is identity-oriented, apply that to $r$ to get $\chi$ identity on $r$'s prime direction; transit with the reciprocal witness via crossEq_symm and crossEq_trans to obtain that the prime direction of $r$ is crossEq its own reciprocal, contradicting primeDirection_not_crossEq_recip.
If every prime is reciprocal-oriented, the symmetric argument on $p$ yields the same self-reciprocal contradiction. No other lemmas are needed.
why it matters
Native cost uniqueness for PRC characters requires that prime-axis calibration not mix identity and reciprocal orientations. This theorem is the pure character-level bridge from the strong (universal) coherence predicate to the existential no-mixing predicate.
Downstream, PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_of_coherent_prime_orientation is a one-line wrapper that applies this result under the prime-calibration target hypotheses. That feeds the uniqueness blocker certificate path (prc_native_cost_uniqueness_blocker_certificate), which packages proved factorization and refutation targets for native cost uniqueness.
In the broader Recognition forcing picture, characters and the $J$-cost (T5) sit under the Recognition Composition Law; keeping prime axes unmixed is part of locking a unique native cost before $\phi$-ladder mass and constant normalizations are read off. The result is fully proved (no sorry).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.