recip_crossEq_zero_iff_crossEq_zero
plain-language theorem explainer
Reciprocal of a ratio orbit is cross-equal to zero exactly when the orbit itself is. Order and reciprocal calculus on the internal PRC rational display cite this equivalence. Proof is a two-step Iff chain through the shared fact that both sides mean the numerator is balanced with the zero signed orbit.
Claim. For every ratio orbit $a$, $\mathrm{crossEq}(\mathrm{recip}(a), 0)$ if and only if $\mathrm{crossEq}(a, 0)$, where cross-equality is the internal cross-multiplication relation on ratio orbits and reciprocal sends zero to zero as in $\mathbb{Q}$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. Cross-equality of two ratio orbits is the internal rational relation: $a$ and $b$ are related when $a.\mathrm{num}\cdot b.\mathrm{den}$ balances $b.\mathrm{num}\cdot a.\mathrm{den}$ as signed orbits (K4.10). It is the PRC stand-in for ordinary rational equality, defined entirely on $\delta$-orbit positions.
The total reciprocal on ratio orbits mirrors $\mathbb{Q}$: if the numerator is balanced with zero, the reciprocal is the zero ratio orbit; otherwise it swaps numerator and denominator in the nonzero branch (K4.12). The dual-recognition symmetry $\iota(x)=x^{-1}$ on the positive reals is the continuous counterpart of this involution.
Two upstream characterizations pin the zero case: cross-equality of $a$ with zero is equivalent to the numerator of $a$ being balanced with the zero signed orbit, and the same holds after taking the reciprocal.
proof idea
Term-mode one-liner. Apply the reciprocal-to-zero characterization (reciprocal cross-equal zero iff numerator balanced with zero), then transitively compose with the symmetric form of the direct characterization (cross-equal zero iff numerator balanced with zero). Both sides reduce to the same signed-orbit balance predicate on $a$'s numerator, so the biconditional closes.
why it matters
Closes a small but necessary reciprocity fact on the zero class of the internal rational order. Downstream, the negation form (reciprocal not cross-equal zero iff original not) is a one-line rewrite of this theorem, and both feed the integer-order certificate that asserts the internal signed-orbit order surface is closed.
In the broader Recognition framework this sits under the reciprocal generator symmetry $\iota(x)=x^{-1}$ that dual-recognition is built on. It does not itself force $J$, $\varphi$, or the eight-tick octave; it is bookkeeping that keeps the PRC rational display coherent under inversion so later order and cost uniqueness results can treat zero and nonzero orbits uniformly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.