ratioOrbit_recip_left_crossEq_iff
plain-language theorem explainer
Cross-equivalence of ratio orbits is symmetric under reciprocal: recip(a) matches b exactly when a matches recip(b). Anyone tracking PRC character reciprocal twists cites this when swapping identity versus reciprocal fixed-point conditions. The proof reduces both sides to rational equality via the verifier display and uses double inversion on ℚ.
Claim. For ratio orbits $a$ and $b$, the internal cross-multiplication relation holds between the reciprocal of $a$ and $b$ if and only if it holds between $a$ and the reciprocal of $b$. Equivalently, writing $[\cdot]$ for the rational verifier display, $[a]^{-1}=[b]$ if and only if $[a]=[b]^{-1}$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. Equality of ratio orbits is not raw structural equality: it is the internal cross-multiplication relation crossEq, which balances scaled numerators and denominators on δ-orbit positions (K4.10). The verifier map toRat sends a ratio orbit to a rational; by design, cross-equivalence agrees with rational equality of those displays.
Reciprocal on ratio orbits is total and mirrors ℚ: zero maps to zero, and nonzero orbits invert. The lemma recip_toRat records that the verifier of a reciprocal is the field inverse of the verifier. The present statement lives in the native-cost uniqueness development, where characters on ratio orbits are compared under reciprocal twists and trace-connectedness constraints.
proof idea
Term-mode rewrite proof. Both sides of the biconditional are rewritten with crossEq_iff_toRat_eq, then each reciprocal is replaced by recip_toRat, so the claim becomes $(a.\mathrm{toRat})^{-1}=b.\mathrm{toRat}$ iff $a.\mathrm{toRat}=(b.\mathrm{toRat})^{-1}$. The two directions are pure field algebra on ℚ: rewrite along the assumed equality and apply inv_inv (double inversion) on the appropriate side.
why it matters
Native-cost uniqueness needs to move freely between a character fixing a prime direction and the same character fixing its reciprocal, after a reciprocal twist. This lemma is the elementary bridge used by the prime and two-prime reciprocal-twist identities (PRCCharacterReciprocalTwist_prime_identity_iff_reciprocal, the matching reciprocal-to-identity forms, and the two-prime analogues), and it feeds the trace-connectedness transfer PRCCharacterTwoPrimeIdentityRespectsTraceConnected_of_reciprocal_twist_reciprocal.
In the broader Recognition stack this is bookkeeping on the rational orbit layer that underwrites cost characters before J-uniqueness (T5) and the Recognition Composition Law are imposed. It does not itself force φ or the octave; it keeps reciprocal symmetry of the internal rational relation coherent so later uniqueness arguments can treat identity and reciprocal fixed points as interchangeable under twist.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.