recip_left_crossEq_of_one_crossEq_mul
plain-language theorem explainer
If two ratio orbits multiply to the unit under cross-multiplication equality, the reciprocal of the first is cross-equal to the second. Order and rational-arithmetic lemmas in the primitive recognition calculus cite this to move between product-one and reciprocal forms. The proof is a one-line wrapper: apply the left-reciprocal form and symmetrize crossEq.
Claim. Let $a,b$ be ratio orbits (signed-orbit numerator over nonzero distinction-nat denominator). If the unit ratio orbit is cross-equal to the product $a\cdot b$ (i.e.\ $1\sim a b$ under balanced cross-multiplication of numerators and denominators), then the reciprocal of $a$ is cross-equal to $b$: $a^{-1}\sim b$.
background
Ratio orbits are the internal PRC display of rationals: a signed orbit numerator over a nonzero distinction-nat denominator (K4.7). Cross-equality crossEq is the native rational relation: two orbits match when the scaled products of numerator and denominator balance as signed orbits (K4.10), the δ-orbit form of cross-multiplication.
Reciprocal on ratio orbits is total and sends the zero orbit to itself, matching the convention on $\mathbb{Q}$ (K4.12). The dual-recognition reciprocal on positive reals is the same involution $x\mapsto x^{-1}$ that the forcing chain builds on.
The module develops integer order and arithmetic entirely on these orbit displays. The immediate upstream lemma already proves that $1\sim a b$ implies $b\sim a^{-1}$; the present statement is the left-reciprocal orientation of that fact.
proof idea
One-line term proof. Apply crossEq_recip_left_of_one_crossEq_mul to $a$, $b$, and the hypothesis $1\sim a b$, obtaining $b\sim a^{-1}$. Then apply crossEq_symm to reverse the cross-equality and conclude $a^{-1}\sim b$. No further unfolding of balance or scaling is required.
why it matters
Feeds the closed integer-order surface certificate (integer_order_certificate), which packages display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity flags. Reciprocal-product identities are needed so that order and comparison on ratio orbits stay compatible with multiplicative inversion when a product hits the unit.
In the Recognition framework this sits in the primitive recognition calculus layer that builds rationals and order from δ-orbits before the forcing chain (T5 J-uniqueness, T6 $\phi$, T7 eight-tick) is stated in continuum language. It is bookkeeping for the internal rational structure, not a continuum forcing step, but without it the order certificate cannot treat reciprocal forms of unit products uniformly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.