PRCCharacterPrimeReciprocalWitnessGlobalizes_of_local_no_mixed_prime_orientation
plain-language theorem explainer
Local prime orientation plus no mixed orientation forces reciprocal-witness globalization: if any prime axis is reciprocal under the character, every prime axis is. Native-cost uniqueness blockers and prime-calibration forcing lemmas cite this. The proof is a short case split on the local orientation of an arbitrary prime against the no-mix hypothesis.
Claim. Let $\chi$ act on rational orbits. Suppose every prime direction is sent by $\chi$ either to itself or to its reciprocal, and $\chi$ never mixes identity orientation on one prime with reciprocal orientation on another. Then: if any prime direction is reciprocal-oriented under $\chi$, every prime direction is reciprocal-oriented under $\chi$.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays (signed numerator over a nonzero distinction denominator). A character $\chi$ is a self-map of ratio orbits used to compare native cost data with doubled-trace data tied to the J-cost $J(x)=(x+x^{-1})/2-1$.
Prime directions are the axes generated by prime distinction orbits. Local prime orientation says each such axis is sent either to itself or to its reciprocal; that is the algebraic content of matching J-costs on a single prime direction. No mixed prime orientation is the trace-coherence ban on choosing identity on one prime and reciprocal on another (independent prime-axis inversions are ruled out).
Reciprocal-witness globalization is the positive branch of that coherence: existence of one reciprocal prime forces every prime axis to be reciprocal. This lemma packages the local-plus-no-mix pair into that global implication.
proof idea
Term-mode case analysis, no external lemmas beyond the three named hypotheses.
Unpack a reciprocal witness prime $p$ and an arbitrary prime $r$. Local orientation on $r$ yields a disjunction: $\chi$ fixes $r$ or sends it to its reciprocal. The identity branch contradicts no-mix against the reciprocal witness $p$, so is eliminated. The remaining branch is exactly reciprocal orientation at $r$. Since $r$ was arbitrary, the existential reciprocal witness globalizes to all primes.
why it matters
This is a coherence step inside native-cost uniqueness for PRC characters. Downstream, the prime-calibration forcing theorem applies it once local orientation is already forced, producing the reciprocal-globalization target under no-mix. That target feeds the native-cost uniqueness blocker certificate and, through the same module chain, the conditional universal-foundation certificate.
In framework terms it supports the T5 J-uniqueness lane: characters that preserve J-cost on prime axes cannot flip primes independently, so the reciprocal branch is all-or-nothing. Without this globalization, mixed prime inversions could produce distinct native costs with the same local J-data, blocking uniqueness of the cost functional built from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.