mul_recip_crossEq_one_of_not_balanced_zero
plain-language theorem explainer
If a ratio orbit has nonzero numerator (not balanced with the zero signed orbit), then multiplying it by its reciprocal yields a ratio orbit cross-equivalent to one. Order and rational-structure proofs in the primitive recognition calculus cite this inverse identity. The proof rewrites the total reciprocal to the nonzero branch and applies the already-proved nonzero reciprocal product lemma.
Claim. Let $a$ be a ratio orbit (signed-orbit numerator over a nonzero distinction-nat denominator). If the numerator of $a$ is not balanced with the zero signed orbit, then the product of $a$ with its reciprocal is cross-equivalent to the unit ratio orbit: $a \cdot a^{-1} \sim_{\times} 1$.
background
In the primitive recognition calculus, integers are carried as signed orbits and rationals as ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator (K4.7). Two signed orbits are balanced when their positive and negative lengths match by $a.pos + b.neg = b.pos + a.neg$ (K4.9); that is the internal integer equality. Two ratio orbits are cross-equivalent when the scaled products of numerator and denominator balance as signed orbits (K4.10), the internal stand-in for rational equality.
Reciprocal on ratio orbits is total, but the productive inverse law needs a nonzero numerator. The sibling recipNonzero packages that hypothesis into the reciprocal construction; a short equality lemma identifies the total recip with recipNonzero precisely when the numerator is not balanced with zero. The product-with-nonzero-reciprocal identity is already proved upstream as mul_recipNonzero_crossEq_one.
proof idea
Term-mode, two steps. First rewrite the total reciprocal via recip_eq_recipNonzero_of_not_balanced_zero, using the hypothesis that the numerator is not balanced with zero, so recip a becomes recipNonzero a h. Then apply mul_recipNonzero_crossEq_one at the same a and h, which already shows that the product with the nonzero reciprocal is cross-equivalent to one. No further arithmetic is unfolded here.
why it matters
This closes the ordinary inverse law $a \cdot a^{-1} \sim 1$ on the ratio-orbit surface under the natural nonzero-numerator guard, so later order and field-structure lemmas can quote the total reciprocal rather than the nonzero branch. Downstream it is used by mul_recip_crossEq_one_of_not_crossEq_zero, which weakens the hypothesis to "not cross-equivalent to zero," and it feeds the aggregate integer_order_certificate that records closure of the internal signed-orbit order surface. In the Recognition foundation stack this is bookkeeping for the rational layer built from $\delta$-orbits before the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$) is invoked; it does not itself force constants, but it keeps the PRC integer/rational displays coherent for those later steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.