zero_not_crossEq_recip_iff_zero_not_crossEq
plain-language theorem explainer
Negation of cross-equivalence to zero is invariant under reciprocal of a ratio orbit: zero fails to match 1/a exactly when it fails to match a. Order-surface and sign-flag proofs cite this when a zero-test must survive a reciprocal flip. Proof is a one-line rewrite of the corresponding positive biconditional.
Claim. For every ratio orbit $a$, the zero orbit fails cross-multiplication equivalence with the reciprocal of $a$ if and only if it fails cross-multiplication equivalence with $a$ itself.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. Cross-equivalence is the internal rational relation of K4.10: two ratio orbits match when the cross-scaled numerator products balance as signed orbits. The total reciprocal on ratio orbits inverts a nonzero display and fixes zero, matching the convention on $\mathbb{Q}$.
The upstream companion states the positive form: zero is cross-equivalent to the reciprocal of $a$ exactly when it is cross-equivalent to $a$. That identity is obtained by routing both sides through the characterization that zero-cross-equivalence means the numerator is balanced to zero. The present statement is the negated form of the same identity, used wherever order or sign flags are phrased as failure of zero-equivalence.
proof idea
One-line wrapper. Rewrite the goal with the positive biconditional that equates cross-equivalence of zero to $\mathrm{recip}(a)$ with cross-equivalence of zero to $a$. Negation is preserved automatically by the rewrite; no further case split is required.
why it matters
Used by the integer-order certificate, which asserts that the internal signed-orbit order surface is closed and packages display lemmas for truncated subtraction, nonnegativity flags, and related order primitives. Reciprocal-invariance of the zero-test is a coherence fact for that surface: comparisons that pass through the dual-recognition reciprocal (the involution $\iota(x)=x^{-1}$ underlying the forcing chain) must not change whether a display is zero. Without the negated form, certificate assembly would re-prove the same rewrite at each call site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.