recip_crossEq_zero_iff_num_balanced_zero
plain-language theorem explainer
For any ratio orbit a, the reciprocal of a is cross-equal to zero exactly when the numerator of a balances the zero signed orbit. Order and rational-structure proofs in the Primitive Recognition Calculus cite this to move zero-tests across reciprocals. The proof is a two-step chain: reduce reciprocal-cross-equality to the reciprocal numerator balancing zero, then cancel the reciprocal on the numerator side.
Claim. For every ratio orbit $a$ (signed-orbit numerator over a nonzero distinction-nat denominator), $\mathrm{crossEq}(\mathrm{recip}(a),\,0)$ if and only if the numerator of $a$ is balanced with the zero signed orbit: $a_{\mathrm{num}}.\mathrm{pos}+0.\mathrm{neg}=0.\mathrm{pos}+a_{\mathrm{num}}.\mathrm{neg}$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits (pairs of distinction-nat lengths) and rationals by ratio orbits: a signed numerator over a nonzero orbit denominator. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that internal relation is the PRC stand-in for integer equality (K4.9).
Two ratio orbits are related by cross-equality when the scaled products $a.\mathrm{num}\cdot b.\mathrm{den}$ and $b.\mathrm{num}\cdot a.\mathrm{den}$ balance as signed orbits (K4.10). Cross-equality is the internal rational equivalence, defined entirely on $\delta$-orbit positions. Reciprocal swaps numerator and denominator (with the usual zero-numerator special case).
The local module builds the order surface on these displays. Two prior facts are used here: cross-equality of any ratio orbit to zero is equivalent to its numerator balancing zero, and the numerator of the reciprocal balances zero exactly when the original numerator does.
proof idea
Term-mode composition of two already-proved biconditionals. First apply the general zero-cross lemma at the reciprocal: $\mathrm{crossEq}(\mathrm{recip}(a),0)\leftrightarrow$ balanced$((\mathrm{recip},a).\mathrm{num},0)$. Then transport across the reciprocal-numerator lemma: balanced$((\mathrm{recip},a).\mathrm{num},0)\leftrightarrow$ balanced$(a.\mathrm{num},0)$. Chain with .trans. No new case analysis.
why it matters
Reciprocals must preserve the zero class if the internal rational order is to be coherent. This lemma is the bridge that lets zero-tests pass through reciprocal: it is cited by the two companion facts that $\mathrm{crossEq}(\mathrm{recip},a,0)$ iff $\mathrm{crossEq}(a,0)$ and iff $\mathrm{crossEq}(0,a)$.
Those facts feed the integer-order certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." Closing that surface is foundation work for Recognition Science: the PRC integer and rational displays underwrite the discrete ledger before the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$) is imposed. Without reciprocal-stable zero detection, the rational layer would not support a well-defined order or equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.