ratioOrbit_recip_recip_crossEq_self
plain-language theorem explainer
Double reciprocal on a ratio orbit is cross-equivalent to the original orbit: recip is an involution up to the internal PRC rational relation. Anyone proving reciprocal-twist identities for ratio characters cites this. The proof transports to verifier rationals, applies recip twice, and uses inv_inv.
Claim. For every ratio orbit $a$, the double reciprocal $\mathrm{recip}(\mathrm{recip}(a))$ is cross-equivalent to $a$: the cross-multiplication relation holds between them (equivalently, their verifier rationals agree).
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. It is the internal display of a rational before any verifier map to $\mathbb{Q}$.
Cross-equivalence is the PRC-native equality of ratio orbits: two orbits match when scaled numerators balance under cross-multiplication on $\delta$-orbit positions. The verifier map toRat sends an orbit to $(n:d)\in\mathbb{Q}$, and cross-equivalence is equivalent to equality of those displays (K4.10).
Reciprocal is total on ratio orbits and sends zero to zero, matching $\mathbb{Q}$. Its verifier law is $(\mathrm{recip},a).\mathrm{toRat}=(a.\mathrm{toRat})^{-1}$. The present lemma is the involution half of that story under the internal relation rather than under toRat alone.
proof idea
Term-mode rewrite chain. First replace cross-equivalence by equality of verifier rationals via crossEq_iff_toRat_eq. Then apply recip_toRat twice so the goal becomes $(a.\mathrm{toRat})^{-1^{-1}}=a.\mathrm{toRat}$. Close with Mathlib inv_inv on the rational display.
why it matters
Native cost uniqueness for PRC ratio characters needs reciprocal to act as a clean involution on the orbit side, not only after transport to $\mathbb{Q}$. This lemma supplies that involution under cross-equivalence.
It is used by the reciprocal-twist character lemmas: the prime and two-prime reciprocal-iff-identity statements, the positive-ratio reciprocal lift from all primes, and the passage from reciprocal-twist trace-connectedness back to identity trace-connectedness. Those results pin when a ratio character is forced to the identity on prime directions, a step toward uniqueness of the native cost (the J-cost side of the forcing chain, T5).
Without double-reciprocal cross-equivalence, twist constructions would not cancel cleanly and the character classification would stall at the reciprocal case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.