PRCCharacterReciprocalTwist_prime_identity_iff_reciprocal
plain-language theorem explainer
For any map χ on ratio orbits and any prime orbit p, the reciprocal twist of χ fixes the prime direction (under cross-equality) if and only if χ itself sends that direction to its reciprocal. Downstream uniqueness and calibration arguments cite this to move identity constraints between a character and its reciprocal twist. The proof is a one-line application of the left-reciprocal cross-equality lemma.
Claim. Let $\chi$ be any map on ratio orbits, and let $p$ be a prime distinction orbit with prime direction $q$. Then $\mathrm{recip}(\chi(q)) \sim q$ if and only if $\chi(q) \sim \mathrm{recip}(q)$, where $\sim$ is cross-multiplication equality of ratio orbits.
background
In the Primitive Recognition Calculus, ratio orbits are the native rational displays: a signed numerator orbit over a nonzero distinction-orbit denominator. Two ratio orbits are related by cross-equality when the scaled numerators balance as signed orbits (the internal stand-in for rational equality). Reciprocal is the total involution on ratio orbits that swaps numerator and denominator (sending zero to zero).
A reciprocal twist of a character $\chi$ is the pointwise composition $\mathrm{recip}\circ\chi$. Prime orbits are the nonzero, non-unit distinction positions with no nontrivial factorization; each carries a canonical prime direction as a ratio orbit. The local module develops native cost uniqueness by comparing characters, their twists, and identity-versus-reciprocal constraints on those prime directions.
proof idea
One-line term proof. Instantiate the general left-reciprocal cross-equality lemma ratioOrbit_recip_left_crossEq_iff at the pair $(\chi(q), q)$, where $q$ is the prime direction of $p$. Unfolding the definition of reciprocal twist, that lemma is exactly the claimed biconditional.
why it matters
This biconditional is the bridge that lets identity constraints on a reciprocal twist be rewritten as reciprocal constraints on the original character (and conversely). Downstream it feeds the admissible prime-identity-iff-two-prime-identity theorem, the force-two theorems that push prime-reciprocal constraints from the twist back to $\chi$, the trace-connected two-prime-reciprocal respect lemma, the prime-calibration target that packages identity-iff-two, and ultimately the native-cost-uniqueness blocker certificate.
In the Recognition forcing picture this is bookkeeping on the character side of native cost uniqueness: it keeps reciprocal symmetry aligned with the J-cost uniqueness story (T5) without leaving the orbit calculus. It does not itself force $\phi$ or the eight-tick structure; it keeps the character lattice consistent under reciprocal duality so those later uniqueness steps can fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.