right_not_crossEq_zero_of_mul_crossEq_one
plain-language theorem explainer
If the product of two ratio orbits is cross-equivalent to one, the right factor is not cross-equivalent to zero. Anyone building reciprocal or multiplicative-inverse lemmas on RatioOrbit cites this side condition. The proof is a one-line projection of the second conjunct from the joint factors lemma.
Claim. Let $a,b$ be ratio orbits. If $a\cdot b$ is cross-equivalent to $1$, then $b$ is not cross-equivalent to $0$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. Cross-equivalence is the internal rational equality: two ratio orbits $a,b$ satisfy crossEq when $a.num\cdot b.den$ balances $b.num\cdot a.den$ as signed orbits (K4.10). Multiplication of ratio orbits is the usual product of fractions on these orbit displays.
The ambient module builds an integer order surface on signed and ratio orbits without leaving the $\delta$-orbit language. The joint upstream result factors_not_crossEq_zero_of_mul_crossEq_one already records that if $a\cdot b$ is cross-equivalent to one, then neither factor is cross-equivalent to zero; the product itself cannot be zero under that hypothesis, and zero-divisors are ruled out on both sides.
proof idea
One-line term wrapper. Apply factors_not_crossEq_zero_of_mul_crossEq_one a b h, which yields the conjunction $\neg\mathrm{crossEq}(a,0)\land\neg\mathrm{crossEq}(b,0)$, and project the second conjunct.
why it matters
This side condition is the right-factor half of the no-zero-divisor fact for units under cross-equivalence. Downstream, crossEq_recip_right_of_mul_crossEq_one uses it to conclude $a$ is cross-equivalent to the reciprocal of $b$ whenever $a\cdot b\sim 1$. The two biconditionals mul_crossEq_one_iff_right_not_crossEq_zero_and_crossEq_recip and mul_crossEq_one_iff_right_not_crossEq_zero_and_recip_crossEq package the same fact into iff characterizations of multiplicative inverses.
Those lemmas feed the closed integer-order certificate (integer_order_certificate), which asserts that the internal signed-orbit order surface is closed. In the Recognition foundation this is bookkeeping for rational arithmetic on orbit displays before the forcing chain (T5 J-uniqueness, T6 $\phi$) is invoked; it does not itself force $\phi$ or the eight-tick structure, but keeps ratio-orbit inversion well-defined on the PRC native cost layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.