recip_crossEq_zero_iff_zero_crossEq
plain-language theorem explainer
For ratio orbits, the reciprocal of a is cross-equal to zero exactly when a itself is cross-equal to zero. Builders of the internal PRC rational order and reciprocal calculus cite this bridge when reducing zero-tests under inversion. The proof is a two-step Iff.trans through the shared fact that both sides mean the numerator balances the zero signed orbit.
Claim. For every ratio orbit $a$, $\mathrm{crossEq}(\mathrm{recip}(a),\,0)\leftrightarrow\mathrm{crossEq}(0,\,a)$, where $\mathrm{crossEq}$ is cross-multiplication equivalence of ratio orbits (signed-orbit balance of scaled numerators against scaled denominators) and $\mathrm{recip}$ is the total reciprocal that sends the zero orbit to itself, as in $\mathbb{Q}$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer (signed-orbit) numerator over a nonzero distinction-nat denominator (K4.7). Two ratio orbits stand in cross-equality when $a.\mathrm{num}$ scaled by $b.\mathrm{den}$ balances $b.\mathrm{num}$ scaled by $a.\mathrm{den}$ as signed orbits; this is the internal PRC rational relation, defined entirely on $\delta$-orbit positions (K4.10).
The total reciprocal on ratio orbits mirrors $\mathbb{Q}$: if the numerator already balances zero, the result is the zero ratio orbit; otherwise numerator and denominator swap (K4.12). The IntegerOrder module builds the order surface on these displays.
Two upstream lemmas pin both sides of the present claim to one atomic condition. Cross-equality of $\mathrm{recip}(a)$ with zero holds iff the numerator of $a$ balances the zero signed orbit; cross-equality of zero with $a$ holds under the same balance. The present theorem simply identifies the two sides.
proof idea
Pure term-mode Iff.trans, no tactics beyond exact. Apply recip_crossEq_zero_iff_num_balanced_zero to rewrite crossEq(recip a, zero) as SignedOrbit.balanced(a.num, zero). Then apply the symmetric form of zero_crossEq_iff_num_balanced_zero, which rewrites that same balance as crossEq(zero, a). The intermediate balance cancels, leaving the biconditional. No case analysis on zero versus nonzero, and no arithmetic beyond the upstream reductions.
why it matters
Immediate consumer is the negated form recip_not_crossEq_zero_iff_zero_not_crossEq, obtained by a single rewrite of this biconditional. Both feed integer_order_certificate, which packages the closed internal signed-orbit order surface (truncated subtraction, leq, abs-diff, and signed nonnegativity display lemmas).
In the broader framework, ratio-orbit reciprocal is the discrete skeleton of the dual-recognition involution $\iota(x)=x^{-1}$ that underwrites the Recognition Composition Law and T5 J-uniqueness. Closing zero-tests under reciprocal on the internal displays is part of making the PRC foundation self-contained before any continuum lift.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.