recip_not_crossEq_zero_iff_zero_not_crossEq
plain-language theorem explainer
Negating both sides of the reciprocal–zero cross-equality, one obtains that the reciprocal of a ratio orbit fails to match zero under cross-multiplication exactly when zero fails to match the original orbit. Order and certificate lemmas that reason about nonzero orbits under reciprocity cite this form. The proof is a one-line rewrite of the positive biconditional.
Claim. For every ratio orbit $a$, $\neg\,\mathrm{crossEq}(\mathrm{recip}(a),0)$ if and only if $\neg\,\mathrm{crossEq}(0,a)$, where $\mathrm{crossEq}$ is the internal cross-multiplication relation on ratio orbits and $\mathrm{recip}$ is the total reciprocal (sending the zero orbit to itself).
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. Two ratio orbits stand in the internal rational relation crossEq when the scaled products of numerator and denominator balance as signed orbits: $a.num\cdot b.den$ balances $b.num\cdot a.den$. This is the PRC stand-in for ordinary rational equality, defined entirely on $\delta$-orbit positions (K4.10).
The total reciprocal on ratio orbits mirrors $\mathbb{Q}$: it sends the zero orbit to itself and otherwise swaps numerator and denominator (K4.12). The positive companion result already records that $\mathrm{crossEq}(\mathrm{recip}(a),0)$ holds exactly when $\mathrm{crossEq}(0,a)$ holds, by routing both sides through numerator-balance-with-zero. The present lemma is the negated packaging of that fact, which order reasoning prefers when excluding the zero class.
proof idea
One-line wrapper: rewrite the goal with the positive biconditional recip_crossEq_zero_iff_zero_crossEq. Negation of both sides of a proved iff is then definitional; no further case analysis on the reciprocal or on balance is required.
why it matters
Feeds the integer-order certificate (integer_order_certificate), whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity flags; the reciprocal–zero exclusion is part of keeping order and sign flags coherent under the total reciprocal.
In the broader Recognition stack this sits in the foundation layer that builds rationals and order from $\delta$-orbits before the forcing chain (T5 J-uniqueness through T8 dimension) is applied. It does not itself force $\phi$ or the eight-tick octave; it closes a small algebraic gap so later order certificates can treat nonzero orbits under reciprocity without reopening cross-multiplication cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.