one_crossEq_recip_mul_of_not_crossEq_zero
plain-language theorem explainer
If a ratio orbit is not cross-equivalent to zero, then the unit orbit is cross-equivalent to the product of its reciprocal with itself. Anyone building the PRC rational field laws or the integer-order certificate cites this. The proof is a one-line symmetry flip of the sibling identity (recip a)·a ~ 1.
Claim. Let $a$ be a ratio orbit (signed-orbit numerator over a nonzero distinction-nat denominator). If $a$ is not cross-equivalent to the zero ratio orbit, then the unit ratio orbit is cross-equivalent to $(\mathrm{recip}\, a)\cdot a$, where cross-equivalence means the two sides balance under cross-multiplication of numerators and denominators as signed orbits.
background
In the Primitive Recognition Calculus, a ratio orbit is the internal stand-in for a rational: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of ratio orbits is not raw structural equality; it is the cross-multiplication relation crossEq, which holds when $a_{\mathrm{num}}\cdot b_{\mathrm{den}}$ balances $b_{\mathrm{num}}\cdot a_{\mathrm{den}}$ as signed orbits (K4.10). That relation is the PRC-native form of rational equality.
Reciprocal on ratio orbits is total and sends the zero class to zero, matching the usual convention on $\mathbb{Q}$ (K4.12). For nonzero $a$, the reciprocal swaps numerator and denominator (with sign bookkeeping). Multiplication of ratio orbits is the ordinary product of fractions at the orbit level.
The sibling result already proves $(\mathrm{recip}, a)\cdot a$ is cross-equivalent to the unit orbit whenever $a$ is not cross-equivalent to zero. The present statement is the same identity with the two sides of crossEq swapped, which is needed wherever the certificate or field axioms demand the unit on the left.
proof idea
One-line term proof. Apply the sibling theorem recip_mul_crossEq_one_of_not_crossEq_zero to obtain
$(\mathrm{recip}, a)\cdot a ;\sim; 1$,
then flip the sides with crossEq_symm (which is just SignedOrbit.balanced_symm under the unfold of cross-equivalence). No further arithmetic is done here.
why it matters
This closes the left-unit form of the multiplicative inverse law for nonzero ratio orbits inside the PRC integer/rational layer. Downstream it is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed; that certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags on signed orbits.
In the broader Recognition stack this sits under the foundation forcing chain: ratio orbits and their reciprocal are the discrete precursors of the dual-recognition involution $\iota(x)=x^{-1}$ used in UniversalForcing, and of the J-cost calculus (T5) that forces $J(x)=\cosh(\log x)-1$. Without a clean $a^{-1}a\sim 1$ identity in both argument orders, the rational display cannot support ordered-field reasoning that later feeds mass-ladder and constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.