recip_not_crossEq_zero_iff_not_crossEq_zero
plain-language theorem explainer
Negating both sides of the reciprocal–zero cross-equivalence yields an iff: a ratio orbit is nonzero under cross-multiplication exactly when its reciprocal is. Order and product lemmas that need nonzero hypotheses on reciprocals cite this. The proof is a one-line rewrite of the positive form of the same equivalence.
Claim. For every ratio orbit $a$, $\neg\,\mathrm{crossEq}(\mathrm{recip}(a),0)$ if and only if $\neg\,\mathrm{crossEq}(a,0)$, where $\mathrm{crossEq}$ is equality of ratio orbits by balanced cross-multiplication of signed numerators and denominators, and $\mathrm{recip}$ is the total reciprocal (sending the zero orbit to itself).
background
In the Primitive Recognition Calculus, a ratio orbit is a signed-orbit numerator over a nonzero distinction-nat denominator. Two ratio orbits stand in the internal rational relation crossEq when the scaled products of numerator and opposite denominator balance as signed orbits (K4.10): this is equality of rationals written entirely on $\delta$-orbit positions.
The total reciprocal on ratio orbits (K4.12) mirrors $\mathbb{Q}$: it sends the zero orbit to itself and otherwise swaps numerator and denominator (with sign bookkeeping). The dual-recognition involution $\iota(x)=x^{-1}$ on positive reals is the continuum counterpart of this discrete reciprocal.
The positive companion already states that $\mathrm{crossEq}(\mathrm{recip}(a),0)$ holds exactly when $\mathrm{crossEq}(a,0)$ holds, by chaining both sides through the numerator-balanced-zero characterization.
proof idea
One-line wrapper: rewrite the goal with the positive equivalence recip_crossEq_zero_iff_crossEq_zero. Negation of both sides of a proved biconditional is then definitional; no further case split or arithmetic is required.
why it matters
Nonzero preservation under reciprocal is the gate for every product and order lemma that assumes both factors (or their reciprocals) avoid the zero orbit. Downstream users include the mul-recip-pair and recip-product nonzero lemmas (both orders of multiplication), the corresponding zero-not-crossEq forms, and ultimately integer_order_certificate, which closes the internal signed-orbit order surface.
Within Recognition Science this sits in the foundation layer that builds an ordered rational display from $\delta$-orbits before the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick) is applied. It is pure rational bookkeeping, not a physics claim, but without it the reciprocal generator cannot be used safely inside order proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.