crossEq_recip_left_of_mul_crossEq_one
plain-language theorem explainer
If the product of two ratio orbits is cross-equivalent to one, the right factor is cross-equivalent to the reciprocal of the left. Order and rational-structure proofs in the primitive recognition calculus cite this when converting a unit product into a reciprocal identity. The proof is a one-line term that feeds the non-zero left factor into the mul-equals-one iff and takes the forward direction.
Claim. For ratio orbits $a,b$, if $a\cdot b$ is cross-equivalent to $1$, then $b$ is cross-equivalent to $a^{-1}$.
background
In the primitive recognition calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator: the internal stand-in for a rational. Two ratio orbits are related by cross-equivalence when the scaled numerators balance as signed orbits ($a.num\cdot b.den$ balances $b.num\cdot a.den$). That relation is the PRC-native equality of rationals, defined entirely on $\delta$-orbit positions.
Reciprocal on ratio orbits is total: it sends the zero orbit to zero and otherwise swaps numerator and denominator in the nonzero case, matching the usual $\mathbb{Q}$ convention. The local module builds the signed-orbit order surface and the arithmetic identities needed to certify that surface.
Upstream, if a product is cross-equivalent to one then neither factor is cross-equivalent to zero; in particular the left factor is nonzero. Separately, under a nonzero-left hypothesis, product cross-equivalent to one is equivalent to the right factor being cross-equivalent to the reciprocal of the left.
proof idea
Term-mode composition of two local lemmas. First apply left_not_crossEq_zero_of_mul_crossEq_one to $h$ to obtain $\neg(a\sim 0)$. Pass that witness into mul_crossEq_one_iff_crossEq_recip_of_left_not_crossEq_zero, which gives the biconditional
$(a\cdot b)\sim 1 \leftrightarrow b\sim a^{-1}$.
Take the forward direction (.mp) on $h$. No further rewriting is needed.
why it matters
This is a directed half of the unit-product characterization for ratio orbits: product equals one forces the right factor to be the reciprocal of the left. Downstream it is reused by the symmetric form with factors swapped in the product, by the left-reciprocal variant via crossEq symmetry, and by the full iff packages that package nonzeroness of factors together with the reciprocal identity.
Those packages feed the integer-order certificate, which closes the internal signed-orbit order surface (truncated subtraction, $\le$, absolute difference, and nonnegativity displays). In the Recognition framework this sits in the foundation layer that makes rational arithmetic and order available before the forcing chain (T5 J-uniqueness, T6 $\phi$, T7 eight-tick, T8 $D=3$) is stated on top of native cost structure. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.