PRCCharacterPrimeIdentityForcesTwoPrimeIdentity_of_local_two_prime_reciprocal_excludes
plain-language theorem explainer
Under local prime orientation, reciprocal orientation of the distinguished orbit-2 axis already rules out identity on every native prime axis, so identity on any prime forces identity on orbit 2. Native-cost uniqueness and the calibration-target ladder cite this one-sided normal form. The proof is a two-branch case split on the local orientation of orbit 2, with the reciprocal branch discharged by contradiction.
Claim. Let $\chi$ act on rational orbits. Assume every prime axis is sent by $\chi$ either to itself or to its reciprocal, and assume that reciprocal orientation of the distinguished orbit-$2$ prime axis excludes identity orientation on every native prime axis. Then, for every prime axis $p$, identity orientation of $p$ under $\chi$ forces identity orientation of the orbit-$2$ prime axis.
background
In the primitive recognition calculus, ratio orbits are rational displays (signed numerator over a nonzero distinction-nat denominator). A character $\chi$ maps ratio orbits to ratio orbits. Prime directions are the axes generated by prime distinction-nats; the distinguished orbit-$2$ axis is the prime direction of the two-step orbit (successor of one), which is itself prime.
Local prime orientation says each prime axis is sent either to itself or to its reciprocal. That is the algebraic content of matching $J$-costs on a single prime direction. The two-prime reciprocal-exclusion hypothesis is the contrapositive branch normal form: if orbit $2$ is reciprocal-oriented, no native prime axis may be identity-oriented.
The target property is the one-sided normal form: identity at any calibrated prime axis forces identity at orbit $2$. The reverse direction is recovered later by applying the same statement to the reciprocal twist of the character. This sits inside the native-cost uniqueness development that pins the recognition cost to the unique $J$ of the forcing chain.
proof idea
Fix a prime $p$ with identity orientation under $\chi$. Apply local orientation at the two-orbit (using that two-orbit is prime) to obtain a disjunction: either $\chi$ fixes the orbit-$2$ axis, or it sends it to its reciprocal.
In the identity branch, the goal is immediate. In the reciprocal branch, feed that reciprocal orientation into the exclusion hypothesis to conclude that no native prime axis can be identity-oriented, contradicting the assumed identity at $p$. Discharge by False.elim. No further lemmas are required beyond the primality of two-orbit.
why it matters
This is the local-to-global bridge that turns a two-specific mixed-witness blocker into the one-sided normal form used throughout native-cost uniqueness. Downstream it packages into the iff with reciprocal exclusion (under local orientation alone), feeds the prime-pair product-cost consistency route to the same normal form, and is the exact lemma applied by the calibration-target theorem that lifts two-prime reciprocal exclusion to the prime-identity-forces-two-prime-identity target.
It also appears in the native-cost uniqueness blocker certificate, which records the zero-calibrated factorization target and the refutation of signed-admissible factorization. In framework terms this is part of locking characters to the unique $J$-cost (T5 / RCL), so that reciprocal twists cannot mix identity and inversion across prime axes without breaking cost coherence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.