recip_num_cmp_zero_of_not_balanced_zero
plain-language theorem explainer
For a rational orbit whose numerator is not balanced with zero, the sign of the reciprocal's numerator equals the sign of the original numerator under the internal signed-orbit comparison. Order theorists building the PRC integer surface cite this when showing reciprocal preserves orientation away from zero. The proof rewrites the total reciprocal to the nonzero branch and applies the already-proved nonzero case.
Claim. Let $a$ be a rational orbit (signed-orbit numerator over a nonzero distinction-nat denominator). If the numerator of $a$ is not balanced with the zero signed orbit, then $\mathrm{cmp}((a^{-1}).\mathrm{num},\,0)=\mathrm{cmp}(a.\mathrm{num},\,0)$, where $\mathrm{cmp}$ is the internal signed-orbit ordering selector.
background
In the Primitive Recognition Calculus, integers are carried as signed orbits: pairs of distinction-nat lengths with an internal balance relation $a.pos+b.neg=b.pos+a.neg$. Two signed orbits are balanced precisely when that length identity holds; balance is the PRC stand-in for integer equality. The internal comparison cmp is defined from that balance test and the nonnegativity flag of the signed difference, not from any external integer display.
A ratio orbit packages a signed-orbit numerator over a nonzero distinction-nat denominator. Reciprocal is defined on ratio orbits; when the numerator is unbalanced with zero it coincides with a dedicated nonzero-reciprocal constructor. The local module builds the order surface on these displays so that later certificates can treat integer and rational order as closed internal structure rather than imported arithmetic.
proof idea
Two-line term proof. First rewrite the total reciprocal along recip_eq_recipNonzero_of_not_balanced_zero, which uses the unbalanced-numerator hypothesis to identify recip a with recipNonzero a h. Then discharge by recipNonzero_num_cmp_zero, which already proves that the nonzero reciprocal preserves cmp of the numerator against zero (by case analysis on that comparison).
why it matters
Feeds integer_order_certificate, the closure theorem stating that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags). Without sign-preservation of reciprocal on nonzero numerators, the rational layer of that certificate would not line up with the signed-orbit order. In the Recognition foundation this is bookkeeping on the integer/rational display stack that underwrites later forcing and ledger constructions; it is not itself a T0–T8 landmark, but it keeps the PRC order surface self-contained so downstream certificates need no external $\mathbb{Z}$ or $\mathbb{Q}$ order axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.