mul_recip_crossEq_one_of_not_crossEq_zero
plain-language theorem explainer
Any nonzero rational orbit multiplies with its reciprocal to the unit orbit under cross-equality. Order and field-structure proofs in the primitive recognition calculus cite this as the internal inverse law for ratio orbits. The argument reduces non-cross-equality with zero to a nonzero numerator, then applies the balanced-numerator inverse lemma.
Claim. Let $a$ be a ratio orbit (signed-orbit numerator over a nonzero distinction-nat denominator). If $a$ is not cross-equal to the zero ratio orbit, then the product of $a$ with its reciprocal is cross-equal to the unit ratio orbit: $a \cdot a^{-1} \sim 1$.
background
In the primitive recognition calculus, integers are carried by signed orbits (pairs of distinction-nat positions) and rationals by ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Two signed orbits are balanced when $a.pos + b.neg = b.pos + a.neg$; this is the internal integer equality (K4.9).
Two ratio orbits are cross-equal when the scaled products $a.num \cdot b.den$ and $b.num \cdot a.den$ balance as signed orbits (K4.10). That relation is the internal rational equality, defined entirely on $\delta$-orbit positions, and it agrees with ordinary rational equality on verifier displays.
Upstream, cross-equality of a ratio orbit with zero is equivalent to its numerator balancing the zero signed orbit. A companion lemma already shows that if the numerator is not balanced with zero, then $a \cdot a^{-1}$ is cross-equal to one (via the nonzero reciprocal construction).
proof idea
Short tactic proof in two steps. First, from $\neg,\mathrm{crossEq}(a,0)$ deduce that the numerator of $a$ is not balanced with the zero signed orbit, by contraposing the iff crossEq_zero_iff_num_balanced_zero. Second, feed that numerator hypothesis into mul_recip_crossEq_one_of_not_balanced_zero, which rewrites the reciprocal to the nonzero form and closes the cross-equality with one.
why it matters
This is the clean inverse law at the ratio-orbit layer: nonzero rationals invert under multiplication up to cross-equality. It feeds the symmetric form one_crossEq_mul_recip_of_not_crossEq_zero and the two-factor product version mul_product_recip_crossEq_one_of_not_crossEq_zero, both needed to treat multiplicative inverses without leaving the $\delta$-orbit language.
Downstream it sits inside the integer-order certificate surface (integer_order_certificate), which packages display lemmas for the closed internal signed-orbit order. In the Recognition foundation stack this is scaffolding for rational arithmetic before the forcing chain (T5 J-uniqueness, T6 $\phi$) is attached; it keeps field-like identities native to orbit positions rather than external $\mathbb{Q}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.