zero_not_crossEq_recip_iff_not_crossEq_zero
plain-language theorem explainer
Negating both sides of the zero–reciprocal cross-equivalence yields an iff: the reciprocal of a ratio orbit is nonzero exactly when the orbit itself is nonzero. Order and product lemmas that need “recip stays away from zero” cite this form. The proof is a one-line rewrite of the positive equivalence.
Claim. For every rational orbit $a$, $\neg\,\mathrm{crossEq}(0, a^{-1})$ 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 reciprocal sends 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 such orbits are related by cross-equivalence when the scaled products of numerator and opposite denominator balance as signed orbits; this is the internal stand-in for rational equality, defined only on $\delta$-orbit positions.
Reciprocal on ratio orbits is total and mirrors $\mathbb{Q}$: the zero orbit maps to zero, and every nonzero orbit swaps numerator and denominator (up to sign bookkeeping). The positive companion states that zero is cross-equivalent to the reciprocal of $a$ exactly when $a$ is cross-equivalent to zero. That fact is proved by chaining two characterizations through “numerator balanced with zero.”
The present module builds the signed-orbit order surface used by the integer-order certificate. Nonzeroness of reciprocals is needed so that products and order comparisons stay inside the nonzero cone.
proof idea
One-line wrapper: rewrite the goal with the positive biconditional zero_crossEq_recip_iff_crossEq_zero, which already equates cross-equivalence of zero with recip a to cross-equivalence of $a$ with zero. Negation of both sides is then definitional; no further case split is required.
why it matters
Feeds the integer-order certificate path and two product lemmas: if $a$ and $b$ are nonzero under cross-equivalence, then the reciprocal of $a\cdot b$ (and of $b\cdot a$) is likewise nonzero. Those lemmas keep multiplicative structure inside the nonzero ratio orbits while the order surface is closed.
In the broader Recognition stack this is bookkeeping on the rational display layer beneath the forcing chain, not a T5–T8 step itself. It ensures reciprocal duality (the same involution that appears as $\iota(x)=x^{-1}$ on positive reals in UniversalForcing) does not collapse nonzero orbits to zero when products are formed. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.