zero_crossEq_recip_iff_zero_crossEq
plain-language theorem explainer
Cross-equality of the zero ratio orbit with the reciprocal of a ratio orbit equals cross-equality of zero with that orbit itself. Rational-order and certificate proofs in the Primitive Recognition Calculus cite this to push zero-tests across the reciprocal involution. The argument is a two-step Iff chain: both sides reduce to the numerator being balanced with signed zero.
Claim. For every ratio orbit $a$, the zero ratio orbit is cross-equivalent to the reciprocal of $a$ if and only if it is cross-equivalent to $a$.
background
In the Primitive Recognition Calculus integer layer, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. Cross-equality is the internal rational relation: two ratio orbits are identified when the cross-multiplied numerators balance as signed orbits (K4.10). The total reciprocal sends a zero numerator to zero and otherwise swaps numerator and denominator, matching the usual $\mathbb{Q}$ convention (K4.12).
Two prior characterizations pin zero under this relation. Zero is cross-equal to $a$ exactly when the numerator of $a$ balances signed zero. Independently, zero is cross-equal to the reciprocal of $a$ under the same numerator-balance condition. The present statement simply equates those two zero-tests.
The local module builds the signed-orbit order surface used by the integer-order certificate; reciprocal symmetry is the dual-recognition involution the broader forcing chain relies on.
proof idea
Term-mode composition of two already-proved biconditionals. Apply the lemma that zero cross-equals the reciprocal of $a$ iff the numerator of $a$ balances signed zero; then transitively compose with the symmetric form of the lemma that zero cross-equals $a$ under the same numerator-balance condition. No case split on zero versus nonzero is needed here: both upstream lemmas already absorb the reciprocal's zero clause.
why it matters
Closes a small but reusable symmetry for zero-tests under reciprocal, so later order facts need not re-expand cross-multiplication. Downstream, the negated form is obtained by a one-line rewrite of this iff, and the integer-order certificate packages the closed signed-orbit order surface (truncated subtraction, $\le$ display, absolute difference, nonnegativity flags). Within Recognition Science this sits in the foundation layer that supports the dual-recognition reciprocal before the forcing chain forces $J$, $\varphi$, the eight-tick octave, and $D=3$; it is bookkeeping on $\delta$-orbit rationals rather than a new physical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.