PRCCharacterReciprocalTwist_prime_reciprocal_iff_identity
plain-language theorem explainer
On any prime ratio-orbit direction, the reciprocal twist of a character χ agrees with ordinary reciprocal if and only if χ itself is the identity there (under cross-multiplication equivalence). Anyone tracking PRC character constraints or native-cost uniqueness cites this biconditional. The proof is a short two-direction term argument: peel one reciprocal via the left-reciprocal crossEq lemma, then cancel double reciprocal, or push identity through reciprocal congruence.
Claim. Let $\chi$ map ratio orbits to ratio orbits, and let $p$ be a prime distinction-nat. Write $q$ for the prime direction of $p$, and write $\tau_\chi(q) := \mathrm{recip}(\chi(q))$ for the reciprocal twist. Then $\tau_\chi(q)$ is cross-multiplication-equivalent to $\mathrm{recip}(q)$ if and only if $\chi(q)$ is cross-multiplication-equivalent to $q$.
background
Primitive Recognition Calculus (PRC) builds rationals from distinction orbits rather than from $\mathbb{Z}$ and $\mathbb{Q}$ as primitives. A RatioOrbit is an integer numerator over a nonzero distinction-nat denominator. Two ratio orbits are related by crossEq when cross-multiplication balances as signed orbits (K4.10): this is the internal PRC stand-in for rational equality.
Reciprocal on ratio orbits is total and sends zero to zero (K4.12). A native prime orbit is a nonzero non-unit distinction-nat with no nontrivial factorization. The prime direction of such a $p$ is the corresponding positive ratio-orbit generator used as a test point for characters.
The reciprocal twist of a map $\chi$ is $\tau_\chi(q) = \mathrm{recip}(\chi(q))$. In the native-cost uniqueness development, characters are constrained on prime directions; this lemma converts an identity constraint on $\chi$ into a reciprocal constraint on $\tau_\chi$, and conversely, without leaving the orbit language.
proof idea
Term-mode constructor on the biconditional.
Forward: assume $\tau_\chi(q)\sim\mathrm{recip}(q)$. Unfold the twist to $\mathrm{recip}(\chi(q))\sim\mathrm{recip}(q)$. The left-reciprocal crossEq equivalence rewrites this as $\chi(q)\sim\mathrm{recip}(\mathrm{recip}(q))$. Transitivity with double-reciprocal recovery ($\mathrm{recip}\circ\mathrm{recip}\sim\mathrm{id}$) yields $\chi(q)\sim q$.
Backward: assume $\chi(q)\sim q$. Reciprocal congruence immediately gives $\mathrm{recip}(\chi(q))\sim\mathrm{recip}(q)$, which is the twist statement after unfolding.
No prime-specific arithmetic is used beyond the type of $q$; primality only fixes the test direction supplied by the caller.
why it matters
Native cost uniqueness in PRC is the orbit-level avatar of J-uniqueness (forcing chain T5): the cost functional satisfying the Recognition Composition Law is forced to be the standard $J$. Characters on ratio orbits are the discrete skeleton of that cost; identity-versus-reciprocal behavior on primes is a standard obstruction pattern.
Downstream, the lemma feeds PRCCharacterPrimeIdentityForcesTwoPrimeIdentity_of_reciprocal_twist_reciprocal_forces_two, which transports a "reciprocal on primes forces the two-prime reciprocal law" hypothesis across the twist into an identity-on-primes forcing statement for $\chi$. It is also referenced by prc_native_cost_uniqueness_blocker_certificate, the certificate object that packages proved factorization targets and refuted signed-admissible alternatives in the uniqueness blocker.
Without this iff, twist duality would not cleanly move prime-point constraints between a character and its reciprocal partner, and the uniqueness certificate chain would stall at the prime-identity step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.