recip_num_not_balanced_zero_iff
plain-language theorem explainer
For any ratio orbit, its reciprocal has a nonzero numerator (in the signed-orbit balance sense) if and only if the original numerator is nonzero. Order and certificate authors cite this when they need the negated form of the reciprocal-zero law. The proof is a one-line rewrite of the positive biconditional.
Claim. For every ratio orbit $a$, the numerator of $\mathrm{recip}(a)$ fails to balance against the zero signed orbit if and only if the numerator of $a$ fails to balance against zero.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction-nat counters (pos, neg) with intended meaning pos - neg. Two signed orbits are balanced when a.pos + b.neg = b.pos + a.neg; balancing against zero is the internal notion of being the zero integer.
A ratio orbit packages a signed-orbit numerator over a nonzero distinction-nat denominator, the PRC display of a rational. Its total reciprocal sends a zero numerator to the zero ratio and otherwise inverts a nonzero ratio, matching the convention on $\mathbb{Q}$.
The sibling theorem recip_num_balanced_zero_iff already records that the reciprocal preserves the zero-numerator property. The present statement is the negated biconditional needed by order lemmas that talk about nonzero numerators.
proof idea
One-line wrapper: rewrite the goal by the positive biconditional recip_num_balanced_zero_iff, which immediately yields the negated form. No case split or unfolding is required here; all work lives in the positive sibling.
why it matters
Feeds the 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 nonnegativity flags on signed orbits. Having both the positive and negated reciprocal-zero laws keeps the order surface free of ad-hoc case analysis when reciprocal appears in comparisons. Locally this is bookkeeping inside the PRC integer/rational layer rather than a forcing-chain step (T5–T8), but it is required infrastructure for any later claim that treats ratio-orbit order as a closed, certified surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.