PRCCharacterNoMixedPrimeOrientation
plain-language theorem explainer
A character on ratio orbits has no mixed prime orientation when it cannot fix one prime axis (identity branch) while inverting another (reciprocal branch). Anyone proving native-cost uniqueness or trace coherence for PRC characters cites this predicate. It is a pure Prop definition: universal quantification over prime orbits with a False conclusion on mixed witnesses.
Claim. A map $\chi$ from ratio orbits to ratio orbits has no mixed prime orientation if, for every pair of prime distinction-orbits $p$ and $r$, it is impossible that $\chi$ is cross-equivalent to the identity on the prime direction of $p$ and simultaneously cross-equivalent to the reciprocal on the prime direction of $r$.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit: a signed-orbit numerator over a nonzero distinction-orbit denominator. Cross-equivalence (crossEq) is the internal PRC stand-in for rational equality via balanced scaled numerators. The total reciprocal on ratio orbits sends a nonzero orbit to its inverse (and zero to zero), matching the reciprocal automorphism of the cost algebra and the reciprocal recognition event in ledger forcing.
A character here is a map $\chi$ on ratio orbits. Prime axes are the prime distinction-orbits; each carries a prime direction. Identity orientation means $\chi$ is cross-equivalent to that direction itself (the J-cost minimum / identity event sits at ratio $1$). Reciprocal orientation means $\chi$ is cross-equivalent to the reciprocal of that direction.
The module develops native-cost uniqueness for PRC characters. Trace coherence requires that prime-axis inversions cannot be chosen independently: fixing one prime while inverting another would break a single global branch choice.
proof idea
Definition only: the body is the Prop that, for all prime orbits $p,r$ with primality witnesses, the conjunction of identity orientation on $p$ and reciprocal orientation on $r$ yields False. No tactics or lemmas; downstream theorems discharge or relate this predicate by intro on the four binders and applying a stronger uniformity or exclusion hypothesis.
why it matters
This is the local trace-coherence gate that rules out independent prime-axis inversions for PRC characters. Downstream, it is equivalent to the existential no-mixed-prime-witnesses form, and it is implied by branch uniformity, by identity-witness exclusion of reciprocal, and by reciprocal-witness globalization. Those implications feed prime-identity branch uniformity and prime-identity trace coherence from local no-mixing.
In the Recognition framework this sits under native-cost uniqueness: characters that match the doubled-trace / J-cost story must pick a single global orientation (identity vs reciprocal) rather than mixing primes. That aligns with the reciprocal automorphism and the identity event at the J-cost minimum, and with the forcing chain demand that the cost law be unique (T5 J-uniqueness, RCL) rather than a product of independent prime flips.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.