recip_crossEq_congr
plain-language theorem explainer
Cross-multiplication equivalence of ratio orbits is preserved by taking reciprocals: if two rational orbit displays agree under cross-multiplication, so do their reciprocals (with zero mapping to zero). Order and arithmetic developers on the PRC integer/rational layer cite this when transporting identities through inversion. The proof is a short rewrite through the verifier display: cross-equivalence is rational equality, and reciprocal matches field inversion on that display.
Claim. Let $a$ and $b$ be ratio orbits (signed-orbit numerator over a nonzero distinction-nat denominator). If $a$ and $b$ are equivalent under cross-multiplication (i.e. $a.n\cdot b.d$ balances $b.n\cdot a.d$ as signed orbits), then the total reciprocals $\mathrm{recip}(a)$ and $\mathrm{recip}(b)$ are likewise cross-multiplication equivalent.
background
In the Primitive Recognition Calculus integer/rational layer, a ratio orbit is a display of a rational: a signed orbit numerator over a nonzero distinction-nat denominator. Cross-multiplication equivalence is the internal PRC rational relation: two ratio orbits are related when the scaled products of numerator and opposite denominator balance as signed orbits. Upstream, that relation is proved equivalent to equality of the verifier rational displays (toRat).
The total reciprocal on ratio orbits sends a zero numerator to zero and otherwise swaps (and re-signs) numerator and denominator, matching ordinary inversion on $\mathbb{Q}$. The companion lemma recip_toRat states that the verifier display of a reciprocal is exactly the field inverse of the original display. The dual-recognition reciprocal on positive reals ($\iota(x)=x^{-1}$) is the continuum counterpart of the same symmetry.
This module builds the signed-orbit order surface on top of those rational primitives; congruence of cross-equivalence under reciprocal is a basic transport fact for that surface.
proof idea
One short tactic proof. Rewrite the hypothesis and the goal with the characterization that cross-multiplication equivalence is equivalent to equality of verifier rationals. Then rewrite both sides of the goal with the display law for reciprocal, which turns each reciprocal into the field inverse of the original display. The hypothesis supplies equality of the original displays, so the inverted displays agree and the goal closes.
why it matters
The result is a congruence lemma for the reciprocal involution on the PRC rational layer. Downstream it feeds the two-way form (cross-equivalence of reciprocals iff cross-equivalence of the originals) and the product-commutation identity that reciprocal of $ab$ is cross-equivalent to reciprocal of $ba$. Both sit inside the integer-order development that closes the signed-orbit order surface (integer_order_certificate).
In the broader Recognition framework, reciprocal symmetry is the dual-recognition involution the forcing chain is built on; keeping cross-multiplication (the native rational equality) stable under that involution is bookkeeping needed before order, cost, and generator arguments can move freely between a ratio and its inverse. It does not itself force $\phi$, the eight-tick octave, or $D=3$, but it is part of the integer/rational substrate those later steps assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.