zero_crossEq_recip_iff_num_balanced_zero
plain-language theorem explainer
Cross-equality of the zero ratio orbit with the reciprocal of a ratio orbit a holds exactly when a's numerator balances the zero signed orbit. Order and rational-identity lemmas in the Primitive Recognition Calculus cite this bridge when relating reciprocal and zero tests. The proof is a one-line composition of the zero-crossEq numerator characterization with reciprocal-numerator balance invariance.
Claim. For every ratio orbit $a$, the zero ratio orbit is cross-equivalent to the reciprocal of $a$ if and only if the numerator of $a$ is balanced with the zero signed orbit (i.e., $a.\mathrm{num}.\mathrm{pos}+0=0+a.\mathrm{num}.\mathrm{neg}$).
background
In the Primitive Recognition Calculus integer layer, a ratio orbit is an integer numerator (a signed orbit of $\delta$-positions) over a nonzero distinction-nat denominator. Two ratio orbits are cross-equivalent when the scaled products of numerator and opposite denominator balance as signed orbits: $a.num\cdot b.den$ balances $b.num\cdot a.den$. That is the internal PRC stand-in for rational equality, defined only on orbit positions (K4.10).
Signed-orbit balance itself is the internal integer relation $a.pos+b.neg=b.pos+a.neg$ (K4.9). The zero ratio orbit and the reciprocal of a ratio orbit are the natural units for testing whether a display is zero or invertible. Upstream, zero cross-equals a ratio orbit exactly when that orbit's numerator balances zero; separately, the numerator of the reciprocal balances zero exactly when the original numerator does.
proof idea
Term-mode one-liner. Apply the zero-crossEq-iff-numerator-balanced characterization to the reciprocal of $a$, then chain (via Iff.trans) the reciprocal-numerator balance invariance, which swaps balance of $(\mathrm{recip},a).num$ against zero for balance of $a.num$ against zero. No case splits or unfolding appear at this site; both legs are already proved.
why it matters
This lemma is the reciprocal-aware zero test used by the sibling bridges that equate zero-crossEq-of-recip with ordinary zero-crossEq and with crossEq-to-zero. Those feed the closed integer-order certificate, whose doc states the internal signed-orbit order surface is closed. In the Recognition foundation stack this keeps rational identity and order entirely on $\delta$-orbit positions, without external $\mathbb{Q}$ or $\mathbb{Z}$ axioms, so later forcing steps (ledger balance, J-cost uniqueness, the eight-tick octave) can treat zero and inversion as internal predicates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.