PRCCharacterTwoPrimeReciprocalForcesPrimeReciprocal_of_local_excludes_prime_identity
plain-language theorem explainer
Under local prime orientation, the exclusion form of the orbit-2 reciprocal branch (no prime may stay identity-oriented) upgrades to the positive forcing form (every prime is reciprocal-oriented). Anyone tracking PRC character branch transport or native-cost uniqueness cites this. The proof is a two-case split on local orientation plus contradiction on the identity arm.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Assume every prime axis is sent by $\chi$ either to itself or to its reciprocal (local prime orientation). Assume also that if the distinguished orbit-$2$ prime axis is reciprocal-oriented, then no native prime axis is identity-oriented. Then if the orbit-$2$ axis is reciprocal-oriented, every native prime axis is reciprocal-oriented.
background
In the Primitive Recognition Calculus, characters act on RatioOrbit displays (signed numerator over nonzero distinction denominator). Prime directions are the native axes of the rational orbit lattice; each may be oriented by $\chi$ either as the identity or as the reciprocal of that axis.
Local prime orientation packages the algebraic content of equal $J$-costs on a single prime direction: for every prime $p$, $\chi$ sends the prime direction either to itself or to its reciprocal. The exclusion hypothesis is the contrapositive branch normal form: reciprocal orientation at the distinguished orbit-$2$ axis forbids any identity-oriented native prime witness.
The target is the positive reciprocal-branch transport normal form: reciprocal orientation at orbit-$2$ forces reciprocal orientation on every native prime axis. This sits inside the native-cost uniqueness development that classifies admissible characters against the $J$-cost and doubled-trace structure.
proof idea
Fix the hypothesis that the orbit-$2$ axis is reciprocal-oriented, and fix an arbitrary prime $p$. Local orientation gives a disjunction: $\chi$ either fixes the prime direction or sends it to its reciprocal.
On the identity arm, apply the exclusion hypothesis at that same $p$ to obtain a contradiction, then eliminate. On the reciprocal arm, the goal is immediate. No further lemmas are needed beyond the two named hypotheses.
why it matters
This is the one-direction bridge from the exclusion normal form to the positive forcing normal form under local orientation. Downstream it is the left-to-right half of the iff equating those two props once local orientation is assumed, and it is applied inside the prime-calibration target that lifts the same transport from the character level to the calibrated uniqueness target.
It also feeds the native-cost uniqueness blocker certificate, which packages the proved factorization and refutation targets that close the uniqueness argument for PRC-native costs. In the broader Recognition chain this is bookkeeping on character orientation coherence that supports uniqueness of the native cost tied to $J$ (T5) rather than a new physical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.