PRCCharacterPrimeIdentityTraceCoherent_of_local_no_mixed_prime_orientation
plain-language theorem explainer
Local prime-axis orientation plus a global ban on mixed identity/reciprocal choices already forces full prime-identity trace coherence: identity on one prime axis implies identity on every prime axis. Native-cost uniqueness arguments cite this to promote per-prime J-cost matching into a cross-prime orientation law. The proof is pure case split on the local disjunction, with the mixed case killed by the no-mix hypothesis.
Claim. Let $\chi$ be a map on rational orbits. Suppose every prime direction is sent by $\chi$ either to itself or to its reciprocal, and suppose $\chi$ never mixes these choices across distinct primes (identity on one prime and reciprocal on another is forbidden). Then identity orientation is trace-coherent: if $\chi$ fixes any prime direction, it fixes every prime direction.
background
In the Primitive Recognition Calculus, ratio orbits package signed integer numerators over nonzero distinction denominators. Characters $\chi$ act on these orbits; the native cost story compares $\chi$ to the identity and reciprocal actions along prime axes, because equality of $J$-costs on a single prime direction only forces the local dichotomy identity-or-reciprocal.
Local prime orientation records that dichotomy for each prime separately: $\chi$ sends the prime direction $p$ to $p$ or to $p^{-1}$. No mixed prime orientation is the cross-prime ban: one cannot have identity on $p$ and reciprocal on $r$ for distinct primes. Prime-identity trace coherence is the missing global relation the local multiplicative and reciprocal character laws do not supply: identity at one calibrated prime forces identity at every calibrated prime.
The module develops uniqueness of the native cost functional built from such characters; the present lemma is the pure propositional bridge from local orientation plus no-mixing to that cross-prime identity transport.
proof idea
Term-mode proof by introduction and case analysis. Fix primes $p,r$ and assume $\chi$ is identity-oriented on $p$. Apply local orientation at $r$: either $\chi$ is identity on $r$, done, or $\chi$ is reciprocal on $r$. The reciprocal branch contradicts no mixed orientation against the identity assumption on $p$, so False.elim closes. No external lemmas beyond the three named predicates.
why it matters
This is the elementary glue step that turns a per-prime $J$-cost match into a coherent global orientation of the prime lattice. Downstream, PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_of_no_mixed_prime_orientation applies it under the calibrated native-cost hypotheses to discharge the prime-identity trace-coherence target once no-mixing is known.
In the Recognition forcing chain this sits under T5 $J$-uniqueness: the cost $J(x)=(x+x^{-1})/2-1$ is insensitive to $x\leftrightarrow x^{-1}$, so characters can flip prime axes independently unless a coherence law forbids mixed flips. The lemma isolates that coherence as a pure logical consequence of local dichotomy plus no-mixing, without invoking the full Recognition Composition Law or the $\phi$-ladder. It closes a scaffolding gap between local prime calibration and the global identity-trace target used in native-cost uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.