primeDirection_not_crossEq_recip
plain-language theorem explainer
A prime distinction orbit never has its directed ratio cross-equivalent to that ratio's reciprocal. Workers on PRC native-cost uniqueness cite this when ruling out mixed identity/reciprocal orientations on primes. The proof rewrites cross-equality as rational equality, forces the underlying natural square equal to 1, hence the natural is 1, contradicting the non-unit half of primality.
Claim. Let $p$ be a prime distinction orbit. Write $r$ for the prime-direction ratio orbit of $p$. Then $r$ is not cross-equivalent to its reciprocal: $\neg\,\mathrm{crossEq}(r, r^{-1})$. Equivalently, if $n$ is the natural display of $p$, then $n\neq 1/n$ as rationals.
background
In the Primitive Recognition Calculus, ratio orbits are internal PRC stand-ins for positive rationals, built from signed $\delta$-orbits (numerator and denominator). Cross-equivalence is the native equality relation: two ratio orbits are cross-equivalent when the scaled numerators balance under cross-multiplication. Upstream, that relation is proved equivalent to equality of the verifier rational displays (crossEq_iff_toRat_eq).
The reciprocal of a ratio orbit swaps and reorients numerator and denominator. A distinction natural carries a toNat display (iteration count from the logic-arithmetic bridge). A prime orbit is a non-unit, non-composite distinction; in particular its natural display is not $1$. The prime-direction construction packages such a prime as a ratio orbit whose rational display is exactly that natural (over $1$).
This lemma lives in the native-cost uniqueness module, which studies ratio characters $\chi$ and the cost functionals they induce, aiming to force the unique J-cost shape.
proof idea
Assume for contradiction that the prime direction is cross-equivalent to its reciprocal. Rewrite via crossEq_iff_toRat_eq, recip_toRat, and primeDirection_toRat to obtain $(n:\mathbb{Q})=1/n$ where $n=p.\mathrm{toNat}$.
First $n\neq 0$: otherwise injectivity of toNat and toNat_zero would make $p$ the zero orbit, contradicting the non-zero half of primeOrbit. Clearing the denominator then yields $n^2=1$ in $\mathbb{Q}$, hence in $\mathbb{N}$.
If $n\ge 2$ then $n^2\ge 4$, contradiction, so $n\le 1$, hence $n=1$. But unit_iff_toNat_eq_one then makes $p$ a unit, contradicting the non-unit half of primeOrbit.
why it matters
Native-cost uniqueness for PRC ratio characters requires that a character cannot treat some primes by identity and others by reciprocal (mixed prime orientation). This elementary non-self-reciprocal fact is the local obstruction used throughout that campaign.
Downstream it is applied in PRCCharacterDistinctPrimeMixedPairWitnesses_absurd_of_branch_uniform, PRCCharacterNoMixedPrimeOrientation_of_branch_uniform, PRCCharacterNoMixedPrimeOrientation_of_reciprocal_witness_globalizes, PRCCharacterNoMixedPrimeWitnesses_of_coherent_prime_orientation, the prime-identity globalization variants, and the admissible-character bridge PRCCharacterPrimeIdentityIffTwoPrimeIdentity_of_admissible. Those results feed the forcing that admissible characters induce the unique doubled-trace/J-cost shape (T5 J-uniqueness in the forcing chain).
Without it, a character could flip a single prime to its reciprocal and still look locally like a cost, breaking uniqueness of the native cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.