zero_crossEq_recip_iff_crossEq_zero
plain-language theorem explainer
Cross-equivalence of the zero ratio orbit with the reciprocal of a is equivalent to cross-equivalence of a with zero. Lemmas that test zero under reciprocal displays in the primitive recognition calculus cite this bridge. The proof is a two-step term chain: both sides reduce to the numerator being balanced with the zero signed orbit.
Claim. For every ratio orbit $a$, the zero orbit is cross-equivalent to the reciprocal of $a$ if and only if $a$ is cross-equivalent to the zero orbit.
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: two ratio orbits match when the scaled products of numerator and opposite denominator balance as signed orbits (cross-multiplication on $\delta$-orbit positions).
The reciprocal on ratio orbits is total and sends zero to zero, matching the convention on $\mathbb{Q}$. Signed-orbit balance against zero is the native zero test on the numerator.
Two prior lemmas already equate each side of the present biconditional to that same numerator-zero test: cross-equivalence of $a$ with zero, and cross-equivalence of zero with the reciprocal of $a$, each hold exactly when the numerator of $a$ balances the zero signed orbit.
proof idea
Term-mode proof by exact. Apply the lemma that zero cross-equivalent to recip($a$) iff the numerator of $a$ is balanced with zero; then transitively compose with the symmetric form of the lemma that $a$ cross-equivalent to zero iff that same numerator balance holds. The shared intermediate proposition cancels, yielding the stated iff.
why it matters
This is a small identity bridge inside the integer-order layer of the primitive recognition calculus. It lets zero-tests be rewritten under reciprocal displays without leaving the cross-equivalence language.
Downstream, the negated form is obtained by a one-line rewrite through this theorem. Both feed 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, order flags, absolute difference, and signed nonnegativity, sealing the order interface used by later forcing and cost uniqueness work.
No open scaffold remains here: the claim is fully proved and sits under the rational-orbit infrastructure (K4.7, K4.10, K4.12) rather than the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.