orbitDirection_nonunit_not_crossEq_recip
plain-language theorem explainer
A nonzero non-unit distinction natural cannot have its orbit direction cross-equivalent to the reciprocal of that direction. Orientation-coherence and branch-agreement arguments for PRC ratio characters cite this exclusion to rule out mixed identity/reciprocal witnesses on non-units. The proof reduces cross-equality to rational equality, forces the squared natural value to equal 1, and recovers the unit case, contradicting the hypothesis.
Claim. Let $p$ be a distinction natural with $p\neq 0$ that is not a unit. Then the ratio orbit given by the orbit direction of $p$ is not cross-equivalent (balanced scaled numerators and denominators in the PRC sense) to the reciprocal of that same orbit direction.
background
The module develops uniqueness of the native cost attached to a PRC ratio character. Ratio orbits are the internal PRC stand-ins for positive rationals, built from signed $\delta$-orbits as numerator and denominator. Cross-equivalence is the native equality relation: two orbits $a,b$ satisfy it when the scaled signed orbits $a.\mathrm{num}\cdot b.\mathrm{den}$ and $b.\mathrm{num}\cdot a.\mathrm{den}$ are balanced. Upstream, that relation is proved equivalent to equality of the verifier displays $a.\mathrm{toRat}=b.\mathrm{toRat}$.
Reciprocal flips a ratio orbit. Orbit direction assigns to a nonzero distinction natural $p$ a canonical ratio orbit (intuitively the ray of $p$). A distinction natural is a unit precisely when its underlying natural value is $1$. The local setting is the non-unit branch of character orientation: one must know that a non-unit direction cannot sit on the same cross-class as its own reciprocal, else the character could mix identity and reciprocal witnesses.
proof idea
Assume cross-equivalence of the orbit direction of $p$ with its reciprocal. Rewrite by the upstream equivalence of cross-equivalence with rational equality, together with the reciprocal and orbit-direction display lemmas, to obtain an equality of rationals $r=1/r$.
From $p\neq 0$ one gets $p.\mathrm{toNat}\neq 0$ (via injectivity of $\mathrm{toNat}$ and $\mathrm{toNat},0=0$), hence the cast to $\mathbb{Q}$ is nonzero. Multiplying the display equality through by that cast and simplifying yields $(p.\mathrm{toNat}:\mathbb{Q})^2=1$, which casts back to $p.\mathrm{toNat}\cdot p.\mathrm{toNat}=1$ in $\mathbb{N}$.
If $p.\mathrm{toNat}\ge 2$ then the product is at least $4$, contradiction, so $p.\mathrm{toNat}\le 1$. Combined with nonzeroness one gets $p.\mathrm{toNat}=1$, which is exactly the unit criterion, contradicting the non-unit hypothesis.
why it matters
This lemma is the elementary arithmetic gate that keeps non-unit orbits from being self-reciprocal. Downstream it is applied inside the coherence and transport packages: no mixed non-unit orbit orientation (from coherence or from identity-branch transport), non-unit branch agreement (from coherence or local identity transport), identity-branch transport itself, and the mixed identity/reciprocal witness reflection theorems that feed prime-local orientation.
Those results sit in the native-cost uniqueness development for PRC ratio characters. The character-to-cost bridge is how the calculus recovers a unique cost matching the doubled-trace/d'Alembert data, which is the PRC-side contribution toward J-uniqueness (forcing step T5: $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. Without excluding self-reciprocal non-units, mixed orientation witnesses would survive and uniqueness of the native cost would fail.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.