crossEq_recip_left_of_one_crossEq_mul
plain-language theorem explainer
If the product of two ratio orbits is cross-equivalent to one, the second orbit is cross-equivalent to the reciprocal of the first. Order and rational-identity lemmas in the PRC integer layer cite this orientation of the reciprocal law. The proof is a one-line wrapper: symmetrize the hypothesis and apply the mul-on-the-left form.
Claim. For ratio orbits $a$ and $b$, if $1$ is cross-equivalent to $a \cdot b$ (cross-multiplication balances as signed orbits), then $b$ is cross-equivalent to the reciprocal of $a$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). Cross-equivalence is the internal rational relation: two ratio orbits satisfy it when the scaled numerators balance as signed orbits under cross-multiplication (K4.10). The reciprocal on ratio orbits is total, sending the zero orbit to zero as in $\mathbb{Q}$ (K4.12).
This module builds the signed-orbit order surface used by the integer-order certificate. The dual-recognition reciprocal on positive reals is the continuum counterpart; here the same involution is realized on discrete ratio orbits.
The sibling lemma already proves the orientation with the product on the left of one: if $a \cdot b$ is cross-equivalent to one, then $b$ is cross-equivalent to $\mathrm{recip}(a)$. Cross-equivalence is symmetric, so the one-on-the-left form is immediate.
proof idea
One-line term wrapper. Apply cross-equivalence symmetry to the hypothesis so that $a \cdot b$ sits on the left of one, then invoke the already-proved lemma that from $a \cdot b \sim 1$ concludes $b \sim \mathrm{recip}(a)$. No new arithmetic is done here.
why it matters
Closes one orientation of the discrete reciprocal identity needed for the internal rational calculus. Downstream, the swapped form (reciprocal on the left) is obtained by another symmetry application, and both feed the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed.
In the Recognition framework this is bookkeeping on the discrete side of dual-recognition symmetry: products that balance to one invert under the ratio-orbit reciprocal, matching the continuum involution $\iota(x)=x^{-1}$ that underpins the Recognition Composition Law and the J-cost uniqueness step (T5). It does not itself force $\phi$ or the eight-tick structure; it keeps the rational layer coherent so later forcing steps can quote order and identity facts without leaving the $\delta$-orbit language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.