ratioOrbit_recip_congr
plain-language theorem explainer
Cross-equivalence of ratio orbits is preserved by the total reciprocal map. Anyone proving that PRC ratio characters respect reciprocal twists or prime-direction identities cites this congruence. The proof is a three-line term rewrite: transport cross-equivalence to rational equality, apply the reciprocal-to-rational identity on both sides, and substitute.
Claim. If two ratio orbits $a$ and $b$ are cross-equivalent (i.e., their cross-multiplied signed numerators balance), then the reciprocal orbits $a^{-1}$ and $b^{-1}$ are likewise cross-equivalent.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Cross-equivalence is the internal PRC rational relation: two orbits are related when the scaled products of numerator and denominator balance as signed orbits. By the K4.10 bridge, this is exactly equality of the verifier rational displays toRat.
The total reciprocal on ratio orbits sends zero to zero and otherwise swaps numerator and denominator in the nonzero case, matching inversion on $\mathbb{Q}$. Its display identity states that the rational of a reciprocal is the reciprocal of the rational. The dual-recognition symmetry $\iota(x)=x^{-1}$ on positive reals is the continuum counterpart of this discrete reciprocal.
This lemma lives in the native-cost uniqueness module, where ratio characters and reciprocal twists must respect the same cross-equivalence that defines the PRC rational structure.
proof idea
One short rewrite chain. First replace both the hypothesis and the goal by the K4.10 equivalence crossEq ↔ toRat equality. Then rewrite each side of the goal with recip_toRat, which turns (recip a).toRat and (recip b).toRat into the ordinary inverses of a.toRat and b.toRat. The hypothesis supplies a.toRat = b.toRat, so the inverted displays agree and cross-equivalence of the reciprocals follows.
why it matters
Native-cost uniqueness needs ratio characters that respect cross-equivalence under reciprocal operations. This congruence is the elementary transport step used by reciprocal-twist identities on prime directions and on the two-prime direction, by the product-reciprocal character theorem, and by the lifts that turn all-prime identity or all-prime reciprocal assumptions into positive-ratio character statements.
Downstream it also feeds the two-prime identity-from-reciprocal-twist implication and appears in the native-cost uniqueness blocker certificate and the refutation of nonunit-orbit local orientation under prime calibration. In the broader forcing picture it keeps the discrete dual-recognition symmetry (reciprocal involution) compatible with the rational orbit calculus that underpins J-cost uniqueness and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.