PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentity_of_two_prime_reciprocal_forces
plain-language theorem explainer
If a ratio-orbit character forces every native prime axis to be reciprocal-oriented whenever the distinguished orbit-2 axis is, then it also excludes identity orientation on every native prime under that same hypothesis. Branch-normal-form arguments in the PRC native-cost uniqueness chain cite this implication. The proof is a short contradiction: identity plus forced reciprocal yields a prime direction cross-equal to its reciprocal, ruled out by the prime-direction non-self-reciprocal lemma.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that whenever $\chi$ sends the distinguished prime axis of $2$ to its reciprocal (up to cross-multiplication equivalence), every native prime axis is likewise sent to its reciprocal. Then, under the same hypothesis on the axis of $2$, no native prime axis may be sent to itself (identity orientation).
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from signed $\delta$-orbits over nonzero distinction denominators. Two ratio orbits are related by crossEq when cross-multiplication balances as signed orbits; this is the internal PRC stand-in for rational equality. Reciprocal is the total involution on ratio orbits (zero fixed), and each native prime $p$ has a distinguished prime direction axis.
Characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ are classified by how they orient these axes: identity-oriented means $\chi$ fixes the axis up to cross-equivalence; reciprocal-oriented means $\chi$ sends it to its reciprocal. The distinguished orbit-$2$ prime axis is the calibration witness for the two-branch normal forms.
The hypothesis package says reciprocal orientation at $2$ forces reciprocal orientation at every native prime. The target package is the contrapositive branch form: reciprocal at $2$ forbids identity orientation at any native prime. Both live in the native-cost uniqueness module that isolates admissible cost characters before J-uniqueness (T5) is recovered.
proof idea
Unfold the target: assume reciprocal orientation at the orbit-$2$ axis, and fix a native prime $p$ claimed identity-oriented. Apply the forcing hypothesis to obtain reciprocal orientation at $p$. Symmetry of cross-equivalence turns the identity witness around; transitivity then yields that the prime direction of $p$ is cross-equivalent to its own reciprocal. The lemma that no prime direction is cross-equal to its reciprocal discharges the contradiction, so identity orientation is impossible.
why it matters
This is one direction of the local equivalence between the "forces all primes reciprocal" normal form and the "excludes any prime identity" normal form, under prime-local orientation. Downstream, the iff theorem packages both directions, and the prime-calibration target theorem lifts the implication to the calibrated uniqueness target used by the native-cost uniqueness blocker certificate.
In the Recognition forcing chain, native cost uniqueness feeds the J-cost identification (T5: $J(x)=(x+x^{-1})/2-1$) by ruling out mixed identity/reciprocal branch characters on prime axes. Closing these branch blockers is scaffolding toward a unique admissible cost before phi, the eight-tick octave, and $D=3$ are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.