recip_num_zero_cmp_of_not_balanced_zero
plain-language theorem explainer
When a rational orbit has nonzero numerator, comparing zero to the numerator of its reciprocal yields the same ordering as comparing zero to the original numerator. Authors of the internal integer-order certificate cite this for reciprocal sign stability under signed-orbit comparison. The proof rewrites the total reciprocal onto the nonzero branch and applies the corresponding comparison lemma.
Claim. Let $a$ be a rational orbit (signed-orbit numerator over a nonzero distinction-natural denominator). If the numerator of $a$ is not balanced with zero, then $\mathrm{cmp}(0,\,\mathrm{num}(a^{-1}))=\mathrm{cmp}(0,\,\mathrm{num}(a))$, where $\mathrm{cmp}$ is the internal signed-orbit comparison selector and two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$.
background
In the Primitive Recognition Calculus, integers appear as signed orbits: pairs of distinction-natural positions that track positive and negative $\delta$-orbit length. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that length identity is the internal PRC integer relation, defined entirely on orbit positions rather than on a verifier display. The comparison selector returns equality on balance and otherwise orders by the nonnegativity flag of the signed difference.
A rational orbit packages a signed-orbit numerator with a nonzero distinction-natural denominator. Reciprocal is defined on every rational orbit, but under the hypothesis that the numerator is unbalanced with zero it coincides with a dedicated nonzero-reciprocal constructor. This lemma sits in the IntegerOrder module that assembles the closed internal order surface for those displays.
Upstream, one result identifies the total reciprocal with the nonzero-reciprocal form under the nonzero hypothesis; another already proves the zero-versus-numerator comparison identity on that nonzero branch by case analysis on $\mathrm{cmp}(0,\mathrm{num}(a))$.
proof idea
Two-step term proof, no fresh case split. Rewrite the total reciprocal along the identification that, under the nonzero-numerator hypothesis, reciprocal equals the nonzero-reciprocal constructor (unfold and simplify on the hypothesis). Then apply exactly the already-proved lemma that zero-versus-numerator comparison is invariant under that nonzero reciprocal. The equality of comparisons is inherited rather than re-derived.
why it matters
Feeds the integer-order certificate, whose statement is that the internal signed-orbit order surface is closed. Reciprocal sign stability is one of the comparison obligations needed so order facts on rational orbits stay coherent when inversion appears in the display layer. Within Recognition Science this is foundation hygiene inside Primitive Recognition Calculus integer and rational scaffolding, upstream of ledger forcing and the T0–T8 chain, not itself a forcing-chain step. It closes a local numerator-sign identity on the path to a certified internal integer order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.